1\DOC top_goal
2
3\TYPE {top_goal : unit -> goal}
4
5\SYNOPSIS
6Returns the current goal of the subgoal package.
7
8\DESCRIBE
9The function {top_goal} is part of the subgoal package. It returns the top goal
10of the goal stack in the current proof state.  For a description of the subgoal
11package, see  {set_goal}.
12
13\FAILURE
14A call to {top_goal} will fail if there are no unproven goals. This could be
15because no goal has been set using {set_goal} or because the last goal set has
16been completely proved.
17
18\USES
19Examining the proof state after a proof fails.
20
21\SEEALSO
22proofManagerLib.set_goal, proofManagerLib.restart,
23proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
24proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
25proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
26
27\ENDDOC
28