--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 13:56:28 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:01 2014 +0200
@@ -1039,8 +1039,8 @@
\item \emph{The Standard ML interfaces are different.} Tools and extensions
written to call the old ML interfaces will need to be adapted to the new
-interfaces. Whenever possible, it is recommended to use
-@{command datatype_compat} to register new-style datatypes as old-style
+interfaces. Whenever possible, it is recommended to use the
+@{command datatype_compat} command to register new-style datatypes as old-style
datatypes.
\item \emph{The recursor @{text rec_t} has a different signature for nested
@@ -1062,17 +1062,20 @@
that unfold the definition of constants introduced by \keyw{datatype} will be
difficult to port.
-\item \emph{Some theorems have different names.}
+\item \emph{Some constants and theorems have different names.}
For non-mutually recursive datatypes,
the alias @{text t.inducts} for @{text t.induct} is no longer generated.
For $m > 1$ mutually recursive datatypes,
+@{text "rec_t\<^sub>1_\<dots>_t\<^sub>m_i"} has been renamed
+@{text "rec_t\<^sub>i"} for each @{text "i \<in> {1, \<dots>, t}"},
@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
-@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}, and similarly the
-collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} has been divided into @{text "t\<^sub>1.size"},
-\ldots, @{text "t\<^sub>m.size"}.
+@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}, and the
+collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} (generated by the
+@{text size} plugin, Section~\ref{ssec:size}) has been divided into
+@{text "t\<^sub>1.size"}, \ldots, @{text "t\<^sub>m.size"}.
\item \emph{The @{text t.simps} collection has been extended.}
-Previously available theorems are available at the same index.
+Previously available theorems are available at the same index as before.
\item \emph{Variables in generated properties have different names.} This is
rarely an issue, except in proof texts that refer to variable names in the