--- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 15 12:46:37 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 15 12:47:16 2016 +0100
@@ -2090,6 +2090,9 @@
text \<open>
\noindent
+For technical reasons, @{text "case"}--@{text "of"} is only supported for
+case distinctions on (co)datatypes that provide discriminators and selectors.
+
Pattern matching is not supported by @{command primcorec}. Fortunately, it is
easy to generate pattern-maching equations using the @{command simps_of_case}
command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
@@ -3462,7 +3465,7 @@
\setlength{\itemsep}{0pt}
\item
-\emph{Defining mutually (co)recursive (co)datatypes is slow.} Fortunately,
+\emph{Defining mutually (co)recursive (co)datatypes can be slow.} Fortunately,
it is always possible to recast mutual specifications to nested ones, which are
processed more efficiently.
@@ -3477,6 +3480,11 @@
\keyw{lemmas} command, is available as an alternative.
\item
+\emph{The \emph{\keyw{primcorec}} command does not allow corecursion under
+@{text "case"}--@{text "of"} for datatypes that are defined without
+discriminators and selectors.
+
+\item
\emph{There is no way to use an overloaded constant from a syntactic type
class, such as @{text 0}, as a constructor.}