--- 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"
--- 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.
--- 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
--- 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;