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