top_goal : unit -> goal
STRUCTURE
SYNOPSIS
Returns the current goal of the subgoal package.
DESCRIPTION
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
HOL  Trindemossen-1