# HG changeset patch
# User desharna
# Date 1404226908 -7200
# Node ID c2ee3f6754c8f880fca28148b97179f5344c644b
# Parent  11cd462e31eced4c34ef2edb7f367ab9cd6d47a2
document property 'rel_induct'

diff -r 11cd462e31ec -r c2ee3f6754c8 src/Doc/Datatypes/Datatypes.thy
--- 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]}