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
32
33
34
35
36
37
38
|
\DOC EXPAND_TAC
\TYPE {EXPAND_TAC : string -> tactic}
\SYNOPSIS
Expand an abbreviation in the hypotheses.
\DESCRIBE
The tactic {EXPAND_TAC "x"}, applied to a goal, looks for a hypothesis of the
form {`t = x`} where {x} is a variable with the given name. It then replaces
{x} by {t} throughout the conclusion of the goal.
\FAILURE
Fails if there is no suitable assumption in the goal.
\EXAMPLE
Consider the final goal in the example given for {ABBREV_TAC}:
{
val it : goalstack = 1 subgoal (1 total)
0 [`12345 + 12345 = n`]
`n + f n = f n`
}
\noindent If we expand it, we get:
{
# e(EXPAND_TAC "n");;
val it : goalstack = 1 subgoal (1 total)
0 [`12345 + 12345 = n`]
`(12345 + 12345) + f (12345 + 12345) = f (12345 + 12345)`
}
\SEEALSO
ABBREV_TAC.
\ENDDOC
|
