
diff -r d4d0bee8c36e -r d066e8369a33 doc-src/IsarRef/Thy/Misc.thy
--- 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




