--- 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").
--- 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}