# HG changeset patch
# User wenzelm
# Date 1354312502 -3600
# Node ID 9149a07a6c6762cc63b1a52d12ce2830653ae341
# Parent  56b4c9afd7be5d0d4ac416d6f2bcf2085f9f3fe8
added 'print_inductives' command;

diff -r 56b4c9afd7be -r 9149a07a6c67 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Nov 30 22:38:06 2012 +0100
+++ b/etc/isar-keywords.el	Fri Nov 30 22:55:02 2012 +0100
@@ -190,6 +190,7 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_inductives"
     "print_interps"
     "print_locale"
     "print_locales"
@@ -413,6 +414,7 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_inductives"
     "print_interps"
     "print_locale"
     "print_locales"
diff -r 56b4c9afd7be -r 9149a07a6c67 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Nov 30 22:38:06 2012 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Fri Nov 30 22:55:02 2012 +0100
@@ -66,6 +66,7 @@
     @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "print_inductives"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def (HOL) mono} & : & @{text attribute} \\
   \end{matharray}
 
@@ -135,6 +136,9 @@
   native HOL predicates.  This allows to define (co)inductive sets,
   where multiple arguments are simulated via tuples.
 
+  \item @{command "print_inductives"} prints (co)inductive definitions and
+  monotonicity rules.
+
   \item @{attribute (HOL) mono} declares monotonicity rules in the
   context.  These rule are involved in the automated monotonicity
   proof of the above inductive and coinductive definitions.
diff -r 56b4c9afd7be -r 9149a07a6c67 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Nov 30 22:38:06 2012 +0100
+++ b/src/HOL/Inductive.thy	Fri Nov 30 22:55:02 2012 +0100
@@ -9,6 +9,7 @@
 keywords
   "inductive" "coinductive" :: thy_decl and
   "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+  "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
 begin
diff -r 56b4c9afd7be -r 9149a07a6c67 src/HOL/Tools/inductive.ML
--- 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;