SPEC_ALL
Drule.SPEC_ALL : thm -> thm
Specializes the conclusion of a theorem with its own quantified variables.
When applied to a theorem A |- !x1...xn. t, the inference rule
SPEC_ALL returns the theorem A |- t[x1'/x1]...[xn'/xn] where the
xi' are distinct variants of the corresponding xi, chosen to avoid
clashes with any variables free in the assumption list and with the
names of constants. Normally xi' is just xi, in which case
SPEC_ALL simply removes all universal quantifiers.
A |- !x1...xn. t
--------------------------- SPEC_ALL
A |- t[x1'/x1]...[xn'/xn]
Failure
Never fails.
Example
> SPEC_ALL CONJ_ASSOC;
val it = ⊢ t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3: thm
See also
Thm.GEN, Thm.GENL,
Drule.GEN_ALL, Tactic.GEN_TAC,
Thm.SPEC, Drule.SPECL,
Tactic.SPEC_TAC