\DOC SPEC_TAC

\TYPE {SPEC_TAC : term * term -> tactic}

\SYNOPSIS
Generalizes a goal.

\KEYWORDS
tactic.

\DESCRIBE
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}.

\USES
Removing unnecessary speciality in a goal, particularly as a prelude to
an inductive proof.

\SEEALSO
Thm.GEN, Thm.GENL, Drule.GEN_ALL, Tactic.GEN_TAC, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.STRIP_TAC.
\ENDDOC