----------------------------------------------------------------------
top_goal                                             (proofManagerLib)
----------------------------------------------------------------------
top_goal : unit -> goal

SYNOPSIS
Returns the current goal of the subgoal package.

DESCRIBE
The function {top_goal} is part of the subgoal package. It returns the top goal
of the goal stack in the current proof state.  For a description of the subgoal
package, see  {set_goal}.

FAILURE
A call to {top_goal} will fail if there are no unproven goals. This could be
because no goal has been set using {set_goal} or because the last goal set has
been completely proved.

USES
Examining the proof state after a proof fails.

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.

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