1\DOC backup
2
3\TYPE {backup : unit -> proof}
4
5\SYNOPSIS
6Restores the proof state, undoing the effects of a previous expansion.
7
8\DESCRIBE
9The function {backup} is part of the subgoal package.  It may be abbreviated by
10the function {b}. It allows backing up from the last state change (caused by
11calls to {expand}, {rotate} and similar functions). The package
12maintains a backup list of previous proof states. A call to {backup}  restores
13the state to the previous state (which was on top of the backup list). The
14current state and the state on top of the backup list are discarded. The
15maximum number of proof states saved on the backup list can be set using
16{set_backup}. It defaults to 15. Adding new proof states after the maximum is reached causes the earliest
17proof state on the list to be discarded. The user may backup repeatedly until
18the list is exhausted.  The state restored includes all unproven subgoals or,
19if a goal had  been proved in the previous state, the corresponding theorem.
20For a description of the subgoal package, see {set_goal}.
21
22\FAILURE
23The function {backup} will fail if the backup list is empty.
24
25\EXAMPLE
26{
27- g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;
28> val it =
29    Proof manager status: 1 proof.
30    1. Incomplete:
31         Initial goal:
32         (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])
33
34     : proofs
35
36- e CONJ_TAC;
37OK..
382 subgoals:
39> val it =
40    TL [1; 2; 3] = [2; 3]
41
42
43    HD [1; 2; 3] = 1
44
45     : proof
46
47- backup();
48> val it =
49    Initial goal:
50
51    (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])
52
53     : proof
54
55- e (REWRITE_TAC[listTheory.HD, listTheory.TL]);
56OK..
57> val it =
58    Initial goal proved.
59    |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]) : proof
60}
61
62
63\USES
64Back tracking in a goal-directed proof to undo errors or try different tactics.
65
66\SEEALSO
67proofManagerLib.set_goal, proofManagerLib.restart,
68proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
69proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
70proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
71
72\ENDDOC
73