--- a/src/HOL/Tools/inductive.ML Fri Nov 30 22:38:06 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Nov 30 22:55:02 2012 +0100
@@ -1167,4 +1167,11 @@
"create simplification rules for inductive predicates"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_inductives"}
+ "print (co)inductive definitions and monotonicity rules"
+ (Scan.succeed
+ (Toplevel.no_timing o Toplevel.unknown_context o
+ Toplevel.keep (print_inductives o Toplevel.context_of)));
+
end;