restart
proofManagerLib.restart : unit -> proof
Returns the proof state to the initial goal.
The function restart is part of the subgoal package. A call to
restart clears the proof history and returns to the initial goal.
After a call to restart, the proof state is the same as it was after
the inital call to set_goal (or g). For a description of the subgoal
package, see set_goal.
Failure
The function restart only fails if no goalstack is being managed.
Restarting an interactive proof.
See also
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.p,
proofManagerLib.top_thm,
proofManagerLib.top_goal