1.1 --- a/src/Doc/Nitpick/document/root.tex	Mon Oct 14 11:07:59 2013 +0200
     1.2 +++ b/src/Doc/Nitpick/document/root.tex	Mon Oct 14 11:14:14 2013 +0200
     1.3 @@ -2794,11 +2794,12 @@
     1.4  \subsection{Registering Coinductive Datatypes}
     1.5  \label{registering-coinductive-datatypes}
     1.6  
     1.7 +Coinductive datatypes defined using the \textbf{codatatype} command that do not
     1.8 +involve nested recursion through non-codatatypes are supported by Nitpick.
     1.9  If you have defined a custom coinductive datatype, you can tell Nitpick about
    1.10 -it, so that it can use an efficient Kodkod axiomatization similar to the one it
    1.11 -uses for lazy lists. The interface for registering and unregistering coinductive
    1.12 -datatypes consists of the following pair of functions defined in the
    1.13 -\textit{Nitpick\_HOL} structure:
    1.14 +it, so that it can use an efficient Kodkod axiomatization. The interface for
    1.15 +registering and unregistering coinductive datatypes consists of the following
    1.16 +pair of functions defined in the \textit{Nitpick\_HOL} structure:
    1.17  
    1.18  \prew
    1.19  $\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
    1.20 @@ -2886,6 +2887,12 @@
    1.21  \item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
    1.22  \textbf{guess} command in a structured proof.
    1.23  
    1.24 +\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} are not
    1.25 +supported.
    1.26 +
    1.27 +\item[\labelitemi] Codatatypes defined using \textbf{codatatype} that
    1.28 +involve nested recursion through non-codatatypes are not supported.
    1.29 +
    1.30  \item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
    1.31  \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
    1.32  improperly.