doc-src/IsarRef/pure.tex

   \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
   \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
 \end{matharray}
 
 These diagnostic commands assist interactive development.  Note that $undo$
 does not apply here, the theory or proof configuration is not changed.
 

   'term' modes? term
   ;
   'prop' modes? prop
   ;
   'typ' modes? type
+  ;
+  'prf' modes? thmrefs?
+  ;
+  'full\_prf' modes? thmrefs?
   ;
 
   modes: '(' (name + ) ')'
   ;
 \end{rail}

   context; the inferred type of $t$ is output as well.  Note that these
   commands are also useful in inspecting the current environment of term
   abbreviations.
 \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
   according to the current theory or proof context.
+\item [$\isarkeyword{prf}$] displays the (compact) proof term of the current
+  proof state (if present), or of the given theorems. Note that this
+  requires proof terms to be switched on for the current object logic
+  (see the ``Proof terms'' section of the Isabelle reference manual
+  for information on how to do this).
+\item [$\isarkeyword{full_prf}$] is like $\isarkeyword{prf}$, but displays
+  the full proof term, i.e.\ also displays information omitted in
+  the compact proof term, which is denoted by ``$_$'' placeholders there.
 \end{descr}
 
 All of the diagnostic commands above admit a list of $modes$ to be specified,
 which is appended to the current print mode (see also \cite{isabelle-ref}).
 Thus the output behavior may be modified according particular print mode