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