1\DOC X_GEN_TAC
2
3\TYPE {X_GEN_TAC : (term -> tactic)}
4
5\SYNOPSIS
6Specializes a goal with the given variable.
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12When applied to a term {x'}, which should be a variable, and a goal
13{A ?- !x. t}, the tactic {X_GEN_TAC} returns the goal {A ?- t[x'/x]}.
14{
15     A ?- !x. t
16   ==============  X_GEN_TAC "x'"
17    A ?- t[x'/x]
18}
19
20
21\FAILURE
22Fails unless the goal's conclusion is universally quantified and the term a
23variable of the appropriate type. It also fails if the variable given is free
24in either the assumptions or (initial) conclusion of the goal.
25
26\SEEALSO
27Tactic.FILTER_GEN_TAC, Thm.GEN, Thm.GENL, Drule.GEN_ALL, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.SPEC_TAC, Tactic.STRIP_TAC.
28\ENDDOC
29