--- a/doc-src/IsarRef/pure.tex Tue Feb 25 12:42:08 2003 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Feb 25 15:27:01 2003 +0100
@@ -1276,6 +1276,8 @@
\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$
@@ -1292,6 +1294,10 @@
;
'typ' modes? type
;
+ 'prf' modes? thmrefs?
+ ;
+ 'full\_prf' modes? thmrefs?
+ ;
modes: '(' (name + ) ')'
;
@@ -1315,6 +1321,14 @@
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,