--- a/src/Doc/Datatypes/Datatypes.thy Wed Oct 07 10:42:13 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Oct 07 13:34:42 2015 +0200
@@ -607,7 +607,10 @@
\item The old-style, nested-as-mutual induction rule and recursor theorems are
generated under their usual names but with ``@{text "compat_"}'' prefixed
(e.g., @{text compat_tree.induct}, @{text compat_tree.inducts}, and
-@{text compat_tree.rec}).
+@{text compat_tree.rec}). These theorems should be identical to the ones
+generated by the old datatype package, \emph{up to the order of the
+premises}---meaning that the subgoals generated by the @{text induct} or
+@{text induction} method may be in a different order than before.
\item All types through which recursion takes place must be new-style datatypes
or the function type.
@@ -1116,14 +1119,16 @@
non-functions) is handled in a more modular fashion. The old-style recursor can
be generated on demand using @{command primrec} if the recursion is via
new-style datatypes, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
+Section~\ref{sssec:primrec-nested-as-mutual-recursion}, or using
+@{command datatype_compat}.
\item \emph{Accordingly, the induction rule is different for nested recursive
-datatypes.} Again, the old-style induction rule can be generated on demand using
-@{command primrec} if the recursion is via new-style datatypes, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}. For recursion through
-functions, the old-style induction rule can be obtained by applying the
-@{text "[unfolded all_mem_range]"} attribute on @{text t.induct}.
+datatypes.} Again, the old-style induction rule can be generated on demand
+using @{command primrec} if the recursion is via new-style datatypes, as
+explained in Section~\ref{sssec:primrec-nested-as-mutual-recursion}, or using
+@{command datatype_compat}. For recursion through functions, the old-style
+induction rule can be obtained by applying the @{text "[unfolded
+all_mem_range]"} attribute on @{text t.induct}.
\item \emph{The @{const size} function has a slightly different definition.}
The new function returns @{text 1} instead of @{text 0} for some nonrecursive