----------------------------------------------------------------------
restore                                              (proofManagerLib)
----------------------------------------------------------------------
restore : unit -> proof

SYNOPSIS
Restores the proof state of the last save point, undoing the effects of expansions after the save point.

DESCRIBE
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
proofManagerLib.set_goal, proofManagerLib.restart,
proofManagerLib.backup, proofManagerLib.restore, proofManagerLib.save,
proofManagerLib.set_backup, proofManagerLib.expand,
proofManagerLib.expandf, proofManagerLib.p, proofManagerLib.top_thm,
proofManagerLib.top_goal.

----------------------------------------------------------------------