top_goal : unit -> term list * term
- 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 CONDITIONS
-
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.
- SEE ALSO
-
b, e, g, p, r, set_goal, top_thm.