# HG changeset patch
# User blanchet
# Date 1410177781 -7200
# Node ID 75b3a5e95d68b7020932e28e1262cc7c9ce131c3
# Parent  3e22d3ed829f6f650bf83ecda6910bae7192eafe
more compatibility documentation

diff -r 3e22d3ed829f -r 75b3a5e95d68 src/Doc/Datatypes/Datatypes.thy
--- 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