1\DOC save
2
3\TYPE {save : unit -> proof}
4
5\SYNOPSIS
6Marks the current proof state as a save point, and clears the automatic undo history.
7
8\DESCRIBE
9The function {save} is part of the subgoal package. A call to
10{save} clears the automatic proof history and marks the current state as
11a save point. A call to {backup} at a save point will fail. In contrast to
12{forget_history}, however, {save} does not clear the initial goal or any
13previous save points. Therefore a call to {restore} or {restart} at a save point
14will succeed.  For a description of the subgoal package, see {set_goal}.
15
16\FAILURE
17The function {save} will fail only if no goalstack is being managed.
18
19\USES
20Creating save points in an interactive proof, to allow user-directed back
21tracking. This is in contrast to the automatic back tracking facilitated by
22{backup}.
23
24\SEEALSO
25proofManagerLib.set_goal, proofManagerLib.restart,
26proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
27proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
28proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
29
30\ENDDOC
31