minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
--- a/src/Doc/Datatypes/Datatypes.thy Wed Oct 02 10:15:53 2013 +0300
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Oct 02 10:34:13 2013 +0200
@@ -1329,8 +1329,8 @@
\item \emph{Theorems sometimes have different names.}
For $m > 1$ mutually recursive functions,
-@{text "f\<^sub>1_\<dots>_f\<^sub>m.simps(k\<^sub>i,\<dots>,k\<^sub>i+n\<^sub>i-1)"} have
-been renamed @{text "f\<^sub>i.simps(1,\<dots>,n\<^sub>i-1)"}.
+@{text "f\<^sub>1_\<dots>_f\<^sub>m.simps"} has been broken down into separate
+subcollections @{text "f\<^sub>i.simps"}.
\end{itemize}
*}