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
31
|
\DOC SPEC_TAC
\TYPE {SPEC_TAC : term * term -> tactic}
\SYNOPSIS
Generalizes a goal.
\KEYWORDS
tactic.
\DESCRIBE
When applied to a pair of terms {(`u`,`x`)}, where {x} is just a variable,
and a goal {A ?- t}, the tactic {SPEC_TAC} generalizes the goal to
{A ?- !x. t[x/u]}, that is, all (free) instances of {u} are turned into {x}.
{
A ?- t
================= SPEC_TAC (`u`,`x`)
A ?- !x. t[x/u]
}
\FAILURE
Fails unless {x} is a variable with the same type as {u}.
\USES
Removing unnecessary speciality in a goal, particularly as a prelude to
an inductive proof.
\SEEALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, STRIP_TAC.
\ENDDOC
|
