src/Doc/Isar_Ref/HOL_Specific.thy

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Apr 03 19:56:51 2015 +0200
@@ -105,6 +105,8 @@
     ;
     clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
     ;
+    @@{command print_inductives} ('!'?)
+    ;
     @@{attribute (HOL) mono} (() | 'add' | 'del')
   \<close>}
 
@@ -137,7 +139,7 @@
   where multiple arguments are simulated via tuples.
 
   \item @{command "print_inductives"} prints (co)inductive definitions and
-  monotonicity rules.
+  monotonicity rules; the ``@{text "!"}'' option indicates extra verbosity.
 
   \item @{attribute (HOL) mono} declares monotonicity rules in the
   context.  These rule are involved in the automated monotonicity