PSPEC_ALL
PairRules.PSPEC_ALL : (thm -> thm)
Specializes the conclusion of a theorem with its own quantified pairs.
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.
See also
Drule.SPEC_ALL,
PairRules.PGEN,
PairRules.PGENL,
PairRules.PGEN_TAC,
PairRules.PSPEC,
PairRules.PSPECL,
PairRules.PSPEC_TAC