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