GEN_TAC : tactic

- STRUCTURE
- SYNOPSIS
- Strips the outermost universal quantifier from the conclusion of a goal.
- DESCRIPTION
- 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.
- USES
- The tactic REPEAT GEN_TAC strips away any universal quantifiers, and is commonly used before tactics relying on the underlying term structure.
- SEEALSO

HOL Kananaskis-14