src/HOL/Tools/inductive.ML
changeset 50302 9149a07a6c67
parent 50301 56b4c9afd7be
child 50771 2852f997bfb5
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 30 22:38:06 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Nov 30 22:55:02 2012 +0100
     1.3 @@ -1167,4 +1167,11 @@
     1.4      "create simplification rules for inductive predicates"
     1.5      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
     1.6  
     1.7 +val _ =
     1.8 +  Outer_Syntax.improper_command @{command_spec "print_inductives"}
     1.9 +    "print (co)inductive definitions and monotonicity rules"
    1.10 +    (Scan.succeed
    1.11 +      (Toplevel.no_timing o Toplevel.unknown_context o
    1.12 +        Toplevel.keep (print_inductives o Toplevel.context_of)));
    1.13 +
    1.14  end;