\DOC save

\TYPE {save : unit -> proof}

\SYNOPSIS
Marks the current proof state as a save point, and clears the automatic undo history.

\DESCRIBE
The function {save} is part of the subgoal package. A call to
{save} clears the automatic proof history and marks the current state as
a save point. A call to {backup} at a save point will fail. In contrast to
{forget_history}, however, {save} does not clear the initial goal or any
previous save points. Therefore a call to {restore} or {restart} at a save point
will succeed.  For a description of the subgoal package, see {set_goal}.

\FAILURE
The function {save} will fail only if no goalstack is being managed.

\USES
Creating save points in an interactive proof, to allow user-directed back
tracking. This is in contrast to the automatic back tracking facilitated by
{backup}.

\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.

\ENDDOC