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