src/Doc/Datatypes/Datatypes.thy

     ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *}
 
 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:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}

 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
 \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
 was internally reduced to mutual recursion. This reduction was visible in the
 type of the recursor, used by \keyw{primrec}. Recursion through functions was

 %
 \[@{thm at_simps(1)[no_vars]}
   \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}):
-*}
-
-    datatype_compat nat
-
-text {* \blankline *}
+restrictions imposed on primitively recursive functions:
+*}
 
     fun at_least_two :: "nat \<Rightarrow> bool" where
       "at_least_two (Succ (Succ _)) \<longleftrightarrow> True" |
       "at_least_two _ \<longleftrightarrow> False"
 

 \emph{There is no way to register the same type as both a datatype and a
 codatatype.} This affects types such as the extended natural numbers, for which
 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.}
 
 \end{enumerate}
 *}

 versions of the package, especially on the coinductive part. Brian Huffman
 suggested major simplifications to the internal constructions. Ond\v{r}ej
 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