1.1 --- a/etc/isar-keywords.el	Fri Nov 30 22:38:06 2012 +0100
     1.2 +++ b/etc/isar-keywords.el	Fri Nov 30 22:55:02 2012 +0100
     1.3 @@ -190,6 +190,7 @@
     1.4      "print_drafts"
     1.5      "print_facts"
     1.6      "print_induct_rules"
     1.7 +    "print_inductives"
     1.8      "print_interps"
     1.9      "print_locale"
    1.10      "print_locales"
    1.11 @@ -413,6 +414,7 @@
    1.12      "print_drafts"
    1.13      "print_facts"
    1.14      "print_induct_rules"
    1.15 +    "print_inductives"
    1.16      "print_interps"
    1.17      "print_locale"
    1.18      "print_locales"

     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Nov 30 22:38:06 2012 +0100
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Fri Nov 30 22:55:02 2012 +0100
     2.3 @@ -66,6 +66,7 @@
     2.4      @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.5      @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.6      @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.7 +    @{command_def "print_inductives"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.8      @{attribute_def (HOL) mono} & : & @{text attribute} \\
     2.9    \end{matharray}
    2.10  
    2.11 @@ -135,6 +136,9 @@
    2.12    native HOL predicates.  This allows to define (co)inductive sets,
    2.13    where multiple arguments are simulated via tuples.
    2.14  
    2.15 +  \item @{command "print_inductives"} prints (co)inductive definitions and
    2.16 +  monotonicity rules.
    2.17 +
    2.18    \item @{attribute (HOL) mono} declares monotonicity rules in the
    2.19    context.  These rule are involved in the automated monotonicity
    2.20    proof of the above inductive and coinductive definitions.

     3.1 --- a/src/HOL/Inductive.thy	Fri Nov 30 22:38:06 2012 +0100
     3.2 +++ b/src/HOL/Inductive.thy	Fri Nov 30 22:55:02 2012 +0100
     3.3 @@ -9,6 +9,7 @@
     3.4  keywords
     3.5    "inductive" "coinductive" :: thy_decl and
     3.6    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
     3.7 +  "print_inductives" :: diag and
     3.8    "rep_datatype" :: thy_goal and
     3.9    "primrec" :: thy_decl
    3.10  begin

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