- STRUCTURE
- SYNOPSIS
Restores the proof state of the last save point, undoing the effects of expansions after the save point.
- DESCRIPTION
The function Backup is part of the subgoal package. A call to Backup
restores the proof state to the last save point (a proof state saved by
save). If the current state is a save point then Backup clears the
current save point and returns to the last save point. If there are no save
points in the history, then Backup returns to the initial goal and is
equivalent to restart. For a description of the subgoal package, see
set_goal.
- FAILURE
The function Backup 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