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
39
40
41
42
43
|
\DOC b
\TYPE {b : unit -> goalstack}
\SYNOPSIS
Restores the proof state, undoing the effects of a previous expansion.
\DESCRIBE
The function {b} is part of the subgoal package. It allows backing up
from the last state change (caused by calls to {e}, {g}, {r}, {set_goal} etc.)
The package maintains a backup list of previous proof states. A call to {b}
restores the state to the previous state (which was on top of the backup list).
\FAILURE
The function {b} will fail if the backup list is empty.
\EXAMPLE
{
# g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;;
val it : goalstack = 1 subgoal (1 total)
`HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`
# e CONJ_TAC;;
val it : goalstack = 2 subgoals (2 total)
`TL [1; 2; 3] = [2; 3]`
`HD [1; 2; 3] = 1`
# b();;
val it : goalstack = 1 subgoal (1 total)
`HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`
}
\USES
Back tracking in a goal-directed proof to undo errors or try different tactics.
\SEEALSO
e, g, p, r, set_goal, top_goal, top_thm.
\ENDDOC
|
