1\DOC restart 2 3\TYPE {restart : unit -> proof} 4 5\SYNOPSIS 6Returns the proof state to the initial goal. 7 8\DESCRIBE 9The function {restart} is part of the subgoal package. A call to {restart} 10clears the proof history and returns to the initial goal. After a call to 11{restart}, the proof state is the same as it was after the inital call to 12{set_goal} (or {g}). For a description of the subgoal package, see {set_goal}. 13 14\FAILURE 15The function {restart} only fails if no goalstack is being managed. 16 17\USES 18Restarting an interactive proof. 19 20\SEEALSO 21proofManagerLib.set_goal, proofManagerLib.restart, 22proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save, 23proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf, 24proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal. 25 26\ENDDOC 27