set_backup
proofManagerLib.set_backup : int -> unit
Limits the number of proof states saved on the subgoal package backup list.
The assignable variable set_backup 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
> set_backup 0;
val it = (): unit
> g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;
val it =
Proof manager status: 5 proofs.
5. Completed goalstack: [.] ⊢ q
4. Completed goalstack: ⊢ HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]
3. Incomplete goalstack:
Initial goal:
HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]
2. Incomplete goalstack:
Initial goal:
HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]
Current goal:
HD [1; 2; 3] = 1
1. Incomplete goalstack:
Initial goal:
HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]
> e CONJ_TAC;
OK..
2 subgoals:
val it =
TL [1; 2; 3] = [2; 3]
HD [1; 2; 3] = 1
> e (REWRITE_TAC[listTheory.HD]);
OK..
Goal proved.
⊢ HD [1; 2; 3] = 1
Remaining subgoals:
val it =
TL [1; 2; 3] = [2; 3]
> b();
val it =
TL [1; 2; 3] = [2; 3]
HD [1; 2; 3] = 1
> b();
val it =
Initial goal:
HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]: proof
See also
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.p,
proofManagerLib.top_thm,
proofManagerLib.top_goal