--- a/doc-src/IsarRef/Thy/Misc.thy Sun Nov 08 13:57:07 2009 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Sun Nov 08 14:38:36 2009 +0100
@@ -21,7 +21,7 @@
\end{matharray}
\begin{rail}
- 'print\_theory' ( '!'?)
+ ('print\_theory' | 'print\_theorems') ('!'?)
;
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
@@ -56,8 +56,8 @@
\item @{command "print_attributes"} prints all attributes
available in the current theory context.
- \item @{command "print_theorems"} prints theorems resulting from
- the last command.
+ \item @{command "print_theorems"} prints theorems resulting from the
+ last command; the ``@{text "!"}'' option indicates extra verbosity.
\item @{command "find_theorems"}~@{text criteria} retrieves facts
from the theory or proof context matching all of given search