# HG changeset patch
# User blanchet
# Date 1411128501 -7200
# Node ID 7179d4da97fc173d68cd1bcd8436ba9b8ddf5e75
# Parent  f0c51576964af1eeac6f1f8ce2e4efb14c8325a8
documented limitations

diff -r f0c51576964a -r 7179d4da97fc src/Doc/Datatypes/Datatypes.thy
--- 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}