1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
\DOC top_thm
\TYPE {top_thm : unit -> thm}
\SYNOPSIS
Returns the theorem just proved using the subgoal package.
\DESCRIBE
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
b, e, g, p, r, set_goal, top_goal.
\ENDDOC
|
