restore : 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 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
HOL  Kananaskis-13