top_goal

proofManagerLib.top_goal : unit -> goal

Returns the current goal of the subgoal package.

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.

Examining the proof state after a proof fails.

See also

proofManagerLib.set_goal, proofManagerLib.restart, proofManagerLib.backup, proofManagerLib.redo, proofManagerLib.restore, proofManagerLib.save, proofManagerLib.set_backup, proofManagerLib.expand, proofManagerLib.expandf, proofManagerLib.p, proofManagerLib.top_thm, proofManagerLib.top_goal