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