SPEC_TAC
Tactic.SPEC_TAC : term * term -> tactic
Generalizes a goal.
When applied to a pair of terms (u,x), where x is just a variable,
and a goal A ?- t, the tactic SPEC_TAC generalizes the goal to
A ?- !x. t[x/u], that is, all instances of u are turned into x.
A ?- t
================= SPEC_TAC (u,x)
A ?- !x. t[x/u]
Failure
Fails unless x is a variable with the same type as u.
Removing unnecessary speciality in a goal, particularly as a prelude to an inductive proof.
See also
Thm.GEN, Thm.GENL,
Drule.GEN_ALL, Tactic.GEN_TAC,
Thm.SPEC, Drule.SPECL,
Drule.SPEC_ALL,
Tactic.STRIP_TAC