# HG changeset patch
# User wenzelm
# Date 1142370389 -3600
# Node ID a86d09815dacc0be6475d2c429b805c922778e0a
# Parent  b98b48496819c276341108eca60947894b6939ca
print_statement;

diff -r b98b48496819 -r a86d09815dac NEWS
--- a/NEWS	Tue Mar 14 16:29:39 2006 +0100
+++ b/NEWS	Tue Mar 14 22:06:29 2006 +0100
@@ -122,6 +122,10 @@
 resulting rule, for later use with the 'cases' method (cf. attribute
 case_names).
 
+* Isar: 'print_statement' prints theorems from the current theory or
+proof context in long statement form, according to the syntax of a
+top-level lemma.
+
 * Isar: 'obtain' takes an optional case name for the local context
 introduction rule (default "that").
 
diff -r b98b48496819 -r a86d09815dac doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Mar 14 16:29:39 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Mar 14 22:06:29 2006 +0100
@@ -832,6 +832,7 @@
 
 \indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}
 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
+\indexisarcmd{print_statement}
 \begin{matharray}{rcl}
   \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
   \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
@@ -840,6 +841,7 @@
   \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
   \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
+  \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
 \end{matharray}
 
 From a theory context, proof mode is entered by an initial goal command such
@@ -874,6 +876,8 @@
   ;
   ('have' | 'show' | 'hence' | 'thus') goal
   ;
+  'print\_statement' modes? thmrefs
+  ;
   
   goal: (props + 'and')
   ;
@@ -924,6 +928,10 @@
   
 \item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''.  Note that $\THUSNAME$
   is also equivalent to ``$\FROM{this}~\SHOWNAME$''.
+  
+\item [$\isarkeyword{print_statement}~\vec a$] prints theorems from
+  the current theory or proof context in long statement form,
+  according to the syntax for $\isarkeyword{lemma}$ given above.
 
 \end{descr}