--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 19 13:41:40 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 19 14:08:21 2014 +0200
@@ -127,8 +127,8 @@
is concerned with the package's interoperability with other Isabelle packages
and tools, such as the code generator, Transfer, Lifting, and Quickcheck.
-%\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
-%Limitations,'' concludes with known open issues at the time of writing.
+\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
+Limitations,'' concludes with known open issues at the time of writing.
\end{itemize}
@@ -2949,35 +2949,59 @@
text {*
The \hthm{extraction} plugin provides realizers for induction and case analysis,
to enable program extraction from proofs involving datatypes. This functionality
-is only available with full proof objects, i.e., with the @{text "HOL-Proofs"}
+is only available with full proof objects, i.e., with the \emph{HOL-Proofs}
session.
*}
-(*
section {* Known Bugs and Limitations
\label{sec:known-bugs-and-limitations} *}
text {*
-Known open issues of the package.
+This section lists the known bugs and limitations in the (co)datatype package at
+the time of this writing. Many of them are expected to be addressed in future
+releases.
+
+\begin{enumerate}
+\setlength{\itemsep}{0pt}
+
+\item
+\emph{Defining mutually (co)recursive (co)datatypes is slow.} Fortunately,
+it is always possible to recast mutual specifications to nested ones, which are
+processed more efficiently.
+
+\item
+\emph{Locally fixed types cannot be used in (co)datatype specifications.}
+This limitation can be circumvented by adding type arguments to the local
+(co)datatypes to abstract over the locally fixed types.
+
+\item
+\emph{The \emph{\keyw{primcorec}} command does not allow user-specified names and
+attributes next to the entered formulas.} The less convenient syntax, using the
+\keyw{lemmas} command, is available as an alternative.
+
+\item
+\emph{There is no way to use an overloaded constant from a syntactic type
+class, such as @{text 0}, as a constructor.}
+
+\item
+\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}
*}
-text {*
-%* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
-%
-%* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
-% (for @{command datatype_compat} and prim(co)rec)
-%
-% * a fortiori, no way to register same type as both data- and codatatype
-%
-%* no recursion through unused arguments (unlike with the old package)
-%
-%* in a locale, cannot use locally fixed types (because of limitation in typedef)?
-%
-% *names of variables suboptimal
-*}
-*)
-
text {*
\section*{Acknowledgment}