top_thm : unit -> thm

- STRUCTURE
- SYNOPSIS
- Returns the theorem just proved using the subgoal package.
- DESCRIPTION
- The function top_thm is part of the subgoal package. A proof state of the package consists of either goal and justification stacks if a proof is in progress or a theorem if a proof has just been completed. If the proof state consists of a theorem, top_thm returns that theorem. For a description of the subgoal package, see set_goal.
- FAILURE
- top_thm will fail if the proof state does not hold a theorem. This will be so either because no goal has been set or because a proof is in progress with unproven subgoals.
- USES
- Accessing the result of an interactive proof session with the subgoal package.
- SEEALSO

HOL Trindemossen-1