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