# HG changeset patch
# User blanchet
# Date 1444217682 -7200
# Node ID c0c8bce2a21b38565ef51892ca5d626d5525970a
# Parent  821ba62ed31b56898be20f99ac6bbbd0f6815590
clarify docs

diff -r 821ba62ed31b -r c0c8bce2a21b src/Doc/Datatypes/Datatypes.thy
--- 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