minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
authorblanchet
Wed, 02 Oct 2013 10:34:13 +0200
changeset 54023 cede3c1d2417
parent 54022 aae0163c01ea
child 54024 07ab4fd922c2
minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
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}
 *}