----------------------------------------------------------------------
GPSPEC                                                     (PairRules)
----------------------------------------------------------------------
GPSPEC : (thm -> thm)

KEYWORDS
rule, genvars.

LIBRARY
pair

SYNOPSIS
Specializes the conclusion of a theorem with unique pairs.

DESCRIBE
When applied to a theorem {A |- !p1...pn. t}, where the number of universally
quantified variables may be zero, {GPSPEC} returns {A |- t[g1/p1]...[gn/pn]},
where the {gi} is paired structures of the same structure as {pi} and
made up of distinct variables , chosen by {genvar}.

        A |- !p1...pn. t
   -------------------------  GPSPEC
    A |- t[g1/p1]...[gn/pn]




FAILURE
Never fails.

USES
{GPSPEC} is useful in writing derived inference rules which need to specialize
theorems while avoiding using any variables that may be present elsewhere.

SEEALSO
Drule.GSPEC, PairRules.PGEN, PairRules.PGENL, Term.genvar,
PairRules.PGEN_TAC, PairRules.PSPEC, PairRules.PSPECL,
PairRules.PSPEC_ALL, PairRules.PSPEC_TAC, PairRules.PSPEC_PAIR.

----------------------------------------------------------------------