FILTER_GEN_TAC

Tactic.FILTER_GEN_TAC : (term -> tactic)

Strips off a universal quantifier, but fails for a given quantified variable.

When applied to a term s and a goal A ?- !x. t, the tactic FILTER_GEN_TAC fails if the quantified variable x is the same as s, but otherwise advances the goal in the same way as GEN_TAC, i.e. returns the goal A ?- t[x'/x] where x' is a variant of x chosen to avoid clashing with any variables free in the goal’s assumption list. Normally x' is just x.

     A ?- !x. t
   ==============  FILTER_GEN_TAC "s"
    A ?- t[x'/x]

Failure

Fails if the goal’s conclusion is not universally quantified or the quantified variable is equal to the given term.

See also

Thm.GEN, Tactic.GEN_TAC, Thm.GENL, Drule.GEN_ALL, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.SPEC_TAC, Tactic.STRIP_TAC