1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\DOC GEN_TAC
\TYPE {GEN_TAC : tactic}
\SYNOPSIS
Strips the outermost universal quantifier from the conclusion of a goal.
\KEYWORDS
tactic, quantifier, universal.
\DESCRIBE
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
GEN, GENL, GEN_ALL, SPEC, SPECL, SPEC_ALL, SPEC_TAC, STRIP_TAC, X_GEN_TAC.
\ENDDOC
|
