- STRUCTURE
- SYNOPSIS
Restores the proof state of the last save point, undoing the effects of expansions after the save point.
- DESCRIPTION
The function restore is part of the subgoal package. A call to restore
restores the proof state to the last save point (a proof state saved by
save). If the current state is a save point then restore clears the
current save point and returns to the last save point. If there are no save
points in the history, then restore returns to the initial goal and is
equivalent to restart. For a description of the subgoal package, see
set_goal.
- FAILURE
The function restore will fail only if no goalstack is being managed.
- USES
Back tracking in a goal-directed proof to a user-defined save point.
- SEEALSO
set_goal,
restart,
backup,
restore,
save,
set_backup,
expand,
expandf,
p,
top_thm,
top_goal