p : unit -> proof
STRUCTURE
SYNOPSIS
Prints the top levels of the subgoal package goal stack.
DESCRIPTION
The function p is part of the subgoal package. For a description of the subgoal package, see set_goal.
FAILURE
Never fails.
USES
Examining the proof state during an interactive proof session.
SEEALSO
HOL  Trindemossen-1