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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
\DOC backup_limit
\TYPE {backup_limit : int}
\SYNOPSIS
Limits the number of proof states saved on the subgoal package backup list.
\DESCRIBE
The assignable variable {backup_limit} is initially set to 12. Its value is one
less than the maximum number of proof states that may be saved on the backup
list. Adding a new proof state (by, for example, a call to {expand}) after the
maximum is reached causes the earliest proof state on the list to be discarded.
For a description of the subgoal package, see {set_goal}.
\EXAMPLE
{
#backup_limit := 0;;
0 : int
#g "(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])";;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])"
() : void
#e CONJ_TAC;;
OK..
2 subgoals
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
#e (REWRITE_TAC[HD]);;
OK..
goal proved
|- HD[1;2;3] = 1
Previous subproof:
"TL[1;2;3] = [2;3]"
() : void
#b();;
2 subgoals
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
#b();;
evaluation failed backup: backup list is empty
}
\SEEALSO
b, backup, e, expand, expandf, g, get_state, p, print_state, r,
rotate, save_top_thm, set_goal, set_state, top_goal, top_thm.
\ENDDOC
|
