--- a/src/Doc/Datatypes/Datatypes.thy Sun Apr 19 15:38:24 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Sun Apr 19 19:29:38 2015 +0200
@@ -604,8 +604,8 @@
text {*
The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
-The command can be useful because the old datatype package provides some
-functionality that is not yet replicated in the new package.
+The command is sometimes useful when migrating from the old datatype package to
+the new one.
A few remarks concern nested recursive datatypes:
@@ -1088,8 +1088,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. If possible, it is recommended to register new-style datatypes as
-old-style datatypes using the @{command datatype_compat} command.
+interfaces. The @{text BNF_LFP_Compat} structure provides convenience functions
+that simulate the old interfaces in terms of the new ones.
\item \emph{The recursor @{text rec_t} has a different signature for nested
recursive datatypes.} In the old package, nested recursion through non-functions
@@ -1256,16 +1256,9 @@
\qquad @{thm at_simps(2)[no_vars]}\]
%
The next example is defined using \keyw{fun} to escape the syntactic
-restrictions imposed on primitively recursive functions. The
-@{command datatype_compat} command is needed to register new-style datatypes
-for use with \keyw{fun} and \keyw{function}
-(Section~\ref{sssec:datatype-compat}):
+restrictions imposed on primitively recursive functions:
*}
- datatype_compat nat
-
-text {* \blankline *}
-
fun at_least_two :: "nat \<Rightarrow> bool" where
"at_least_two (Succ (Succ _)) \<longleftrightarrow> True" |
"at_least_two _ \<longleftrightarrow> False"
@@ -3218,12 +3211,6 @@
both views would make sense (for a different set of constructors).
\item
-\emph{The \emph{\keyw{derive}} command from the \emph{Archive of Formal Proofs}
-has not yet been fully ported to the new-style datatypes.} Specimens featuring
-nested recursion require the use of @{command datatype_compat}
-(Section~\ref{sssec:datatype-compat}).
-
-\item
\emph{The names of variables are often suboptimal in the properties generated by
the package.}
@@ -3241,8 +3228,9 @@
Kun\v{c}ar implemented the @{text transfer} and @{text lifting} plugins.
Florian Haftmann and Christian Urban provided general advice on Isabelle and
package writing. Stefan Milius and Lutz Schr\"oder found an elegant proof that
-eliminated one of the BNF proof obligations. Andreas Lochbihler, Tobias Nipkow,
-and Christian Sternagel suggested many textual improvements to this tutorial.
+eliminated one of the BNF proof obligations. Gerwin Klein, Andreas Lochbihler,
+Tobias Nipkow, and Christian Sternagel suggested many textual improvements to
+this tutorial.
*}
end