1\DOC p
2
3\TYPE {p : unit -> proof}
4
5\SYNOPSIS
6Prints the top levels of the subgoal package goal stack.
7
8\DESCRIBE
9The function {p} is part of the subgoal package. For a description of
10the subgoal package, see {set_goal}.
11
12\FAILURE
13Never fails.
14
15\USES
16Examining the proof state during an interactive proof session.
17
18\SEEALSO
19proofManagerLib.set_goal, proofManagerLib.restart, proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save, proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf, proofManagerLib.p,proofManagerLib.top_thm, proofManagerLib.top_goal.
20
21\ENDDOC
22