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