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