1\DOC FILTER_GEN_TAC 2 3\TYPE {FILTER_GEN_TAC : (term -> tactic)} 4 5\SYNOPSIS 6Strips off a universal quantifier, but fails for a given quantified variable. 7 8\KEYWORDS 9tactic, selective, quantifier, universal. 10 11\DESCRIBE 12When applied to a term {s} and a goal {A ?- !x. t}, the tactic {FILTER_GEN_TAC} 13fails if the quantified variable {x} is the same as {s}, but otherwise 14advances the goal in the same way as {GEN_TAC}, i.e. returns the goal 15{A ?- t[x'/x]} where {x'} is a variant of {x} chosen to avoid clashing with 16any variables free in the goal's assumption list. Normally {x'} is just {x}. 17{ 18 A ?- !x. t 19 ============== FILTER_GEN_TAC "s" 20 A ?- t[x'/x] 21} 22 23 24\FAILURE 25Fails if the goal's conclusion is not universally quantified or the 26quantified variable is equal to the given term. 27 28\SEEALSO 29Thm.GEN, Tactic.GEN_TAC, Thm.GENL, Drule.GEN_ALL, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.SPEC_TAC, Tactic.STRIP_TAC. 30\ENDDOC 31