# HG changeset patch
# User blanchet
# Date 1380702853 -7200
# Node ID cede3c1d2417fc9e2ff947dbdb3c7db6018c259a
# Parent  aae0163c01eaf5996f69f1883188613f504c477a
minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)

diff -r aae0163c01ea -r cede3c1d2417 src/Doc/Datatypes/Datatypes.thy
--- 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}
 *}