saveproofManagerLib.save : unit -> proofMarks the current proof state as a save point, and clears the automatic undo history.
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.
The function save will fail only if no goalstack is
being managed.
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.
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