----------------------------------------------------------------------
PSPEC_ALL                                                  (PairRules)
----------------------------------------------------------------------
PSPEC_ALL : (thm -> thm)

KEYWORDS
rule.

LIBRARY
pair

SYNOPSIS
Specializes the conclusion of a theorem with its own quantified pairs.

DESCRIBE
When applied to a theorem {A |- !p1...pn. t}, the inference rule {PSPEC_ALL}
returns the theorem {A |- t[p1'/p1]...[pn'/pn]} where the {pi'} are distinct
variants of the corresponding {pi}, chosen to avoid clashes with any variables
free in the assumption list and with the names of constants. Normally {pi'} is
just {pi}, in which case {PSPEC_ALL} simply removes all universal quantifiers.

       A |- !p1...pn. t
   ---------------------------  PSPEC_ALL
    A |- t[p1'/x1]...[pn'/xn]




FAILURE
Never fails.

SEEALSO
Drule.SPEC_ALL, PairRules.PGEN, PairRules.PGENL, PairRules.PGEN_TAC,
PairRules.PSPEC, PairRules.PSPECL, PairRules.PSPEC_TAC.

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