GEN_TAC
Tactic.GEN_TAC : tactic
Strips the outermost universal quantifier from the conclusion of a goal.
When applied to a goal A ?- !x. t, the tactic GEN_TAC reduces it to
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
============== GEN_TAC
A ?- t[x'/x]
Failure
Fails unless the goal's conclusion is universally quantified.
The tactic REPEAT GEN_TAC strips away any universal quantifiers, and
is commonly used before tactics relying on the underlying term
structure.
See also
Tactic.FILTER_GEN_TAC,
Thm.GEN, Thm.GENL,
Drule.GEN_ALL, Thm.SPEC,
Drule.SPECL, Drule.SPEC_ALL,
Tactic.SPEC_TAC,
Tactic.STRIP_TAC,
Tactic.X_GEN_TAC