Backup : unit -> proof
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
HOL  Kananaskis-10