p
proofManagerLib.p : unit -> proof
Prints the top levels of the subgoal package goal stack.
The function p is part of the subgoal package. For a description of
the subgoal package, see set_goal.
Failure
Never fails.
Examining the proof state during an interactive proof session.
See also
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.p,
proofManagerLib.top_thm,
proofManagerLib.top_goal