- STRUCTURE
- SYNOPSIS
Marks the current proof state as a save point, and clears the automatic undo history.
- DESCRIPTION
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
set_goal,
restart,
backup,
restore,
save,
set_backup,
expand,
expandf,
p,
top_thm,
top_goal