----------------------------------------------------------------------
set_backup                                           (proofManagerLib)
----------------------------------------------------------------------
proofManagerLib.set_backup : int -> unit

SYNOPSIS
Limits the number of proof states saved on the subgoal package backup list.

DESCRIBE
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;
()  unit

- g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])

     : proofs

- e CONJ_TAC;
OK..
2 subgoals:
> val it =
    TL [1; 2; 3] = [2; 3]


    HD [1; 2; 3] = 1

     :proof

- e (REWRITE_TAC[listTheory.HD]);
OK..

Goal proved.
|- HD [1; 2; 3] = 1

Remaining subgoals:
> val it =
    TL [1; 2; 3] = [2; 3]

     : proof

- b();
> val it =
    TL [1; 2; 3] = [2; 3]


    HD [1; 2; 3] = 1

     : proof

- b();
! Uncaught exception:
! CANT_BACKUP_ANYMORE




SEEALSO
proofManagerLib.set_goal, proofManagerLib.restart,
proofManagerLib.backup, proofManagerLib.restore, proofManagerLib.save,
proofManagerLib.set_backup, proofManagerLib.expand,
proofManagerLib.expandf, proofManagerLib.p, proofManagerLib.top_thm,
proofManagerLib.top_goal.

----------------------------------------------------------------------