# HG changeset patch
# User berghofe
# Date 1046183221 -3600
# Node ID c690cb885db4a2edfabd5ef110428bc81a09ca40
# Parent  e94aa103e12d5214fced6fa54738e189652ab560
Documented prf / full_prf commands and antiquotations.

diff -r e94aa103e12d -r c690cb885db4 doc-src/IsarRef/pure.tex
--- 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,
diff -r e94aa103e12d -r c690cb885db4 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Tue Feb 25 12:42:08 2003 +0100
+++ b/doc-src/IsarRef/syntax.tex	Tue Feb 25 15:27:01 2003 +0100
@@ -410,6 +410,8 @@
   text & : & \isarantiq \\
   goals & : & \isarantiq \\
   subgoals & : & \isarantiq \\
+  prf & : & \isarantiq \\
+  full_prf & : & \isarantiq \\
 \end{matharray}
 
 The text body of formal comments (see also \S\ref{sec:comments}) may contain
@@ -440,7 +442,9 @@
     'typ' options type |
     'text' options name |
     'goals' options |
-    'subgoals' options
+    'subgoals' options |
+    'prf' options thmrefs |
+    'full\_prf' options thmrefs
   ;
   options: '[' (option * ',') ']'
   ;
@@ -478,6 +482,16 @@
 \item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
   print the main goal.
 
+\item [$\at\{prf~\vec a\}$] prints the (compact) proof terms corresponding to
+  the theorems $\vec a$. 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 [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays
+  the full proof terms, i.e.\ also displays information omitted in
+  the compact proof term, which is denoted by ``$_$'' placeholders there.
+
 \end{descr}
 
 \medskip