1\DOC top_thm
2
3\TYPE {top_thm : unit -> thm}
4
5\SYNOPSIS
6Returns the theorem just proved using the subgoal package.
7
8\DESCRIBE
9The function {top_thm} is part of the subgoal package. A proof state of the
10package consists of either  goal and justification stacks if a proof is in
11progress or a theorem if a proof has just been completed. If the proof state
12consists of a theorem, {top_thm} returns that theorem. For a description of the
13subgoal package, see {set_goal}.
14
15\FAILURE
16{top_thm} will fail if the proof state does not hold a theorem. This will be
17so either because no goal has been set or because a proof is in progress with
18unproven subgoals.
19
20\USES
21Accessing the result of an interactive proof session with the subgoal package.
22
23\SEEALSO
24proofManagerLib.set_goal, proofManagerLib.restart,
25proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
26proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
27proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
28
29\ENDDOC
30