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