1\DOC SPEC_TAC 2 3\TYPE {SPEC_TAC : term * term -> tactic} 4 5\SYNOPSIS 6Generalizes a goal. 7 8\KEYWORDS 9tactic. 10 11\DESCRIBE 12When applied to a pair of terms {(u,x)}, where {x} is just a variable, 13and a goal {A ?- t}, the tactic {SPEC_TAC} generalizes the goal to 14{A ?- !x. t[x/u]}, that is, all instances of {u} are turned into {x}. 15{ 16 A ?- t 17 ================= SPEC_TAC (u,x) 18 A ?- !x. t[x/u] 19} 20 21 22\FAILURE 23Fails unless {x} is a variable with the same type as {u}. 24 25\USES 26Removing unnecessary speciality in a goal, particularly as a prelude to 27an inductive proof. 28 29\SEEALSO 30Thm.GEN, Thm.GENL, Drule.GEN_ALL, Tactic.GEN_TAC, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.STRIP_TAC. 31\ENDDOC 32