doc-src/IsarRef/pure.tex

 
 \subsection{Goal statements}\label{sec:goals}
 
 \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)} \\
   \isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\
   \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   \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
 as $\LEMMANAME$, $\THEOREMNAME$, or $\COROLLARYNAME$.  Within a proof, new
 claims may be introduced locally as well; four variants are available here to

 \begin{rail}
   ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
   ;
   ('have' | 'show' | 'hence' | 'thus') goal
   ;
+  'print\_statement' modes? thmrefs
+  ;
   
   goal: (props + 'and')
   ;
   longgoal: thmdecl? (contextelem *) conclusion
   ;

   goal to be proven by forward chaining the current facts.  Note that
   $\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''.
   
 \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}
 
 Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
 be bound automatically, see also \S\ref{sec:term-abbrev}.  Furthermore, the