--- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 01 17:01:28 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 01 17:01:48 2014 +0200
@@ -948,6 +948,13 @@
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
prove $m$ properties simultaneously.
+\item[@{text "t."}\hthm{rel\_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct pred]"}\rm:] ~ \\
+@{thm list.rel_induct[no_vars]}
+
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel\_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
+prove $m$ properties simultaneously.
+
\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}