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