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