--- a/src/Doc/Nitpick/document/root.tex Mon Oct 14 11:07:59 2013 +0200
+++ b/src/Doc/Nitpick/document/root.tex Mon Oct 14 11:14:14 2013 +0200
@@ -2794,11 +2794,12 @@
\subsection{Registering Coinductive Datatypes}
\label{registering-coinductive-datatypes}
+Coinductive datatypes defined using the \textbf{codatatype} command that do not
+involve nested recursion through non-codatatypes are supported by Nitpick.
If you have defined a custom coinductive datatype, you can tell Nitpick about
-it, so that it can use an efficient Kodkod axiomatization similar to the one it
-uses for lazy lists. The interface for registering and unregistering coinductive
-datatypes consists of the following pair of functions defined in the
-\textit{Nitpick\_HOL} structure:
+it, so that it can use an efficient Kodkod axiomatization. The interface for
+registering and unregistering coinductive datatypes consists of the following
+pair of functions defined in the \textit{Nitpick\_HOL} structure:
\prew
$\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
@@ -2886,6 +2887,12 @@
\item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.
+\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} are not
+supported.
+
+\item[\labelitemi] Codatatypes defined using \textbf{codatatype} that
+involve nested recursion through non-codatatypes are not supported.
+
\item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
\textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
improperly.