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