1.1 --- a/doc-src/Nitpick/nitpick.tex	Wed Feb 17 13:57:45 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Wed Feb 17 14:11:41 2010 +0100
     1.3 @@ -2080,9 +2080,10 @@
     1.4  {\small See also \textit{mono} (\S\ref{scope-of-search}).}
     1.5  
     1.6  \opargbool{std}{type}{non\_std}
     1.7 -Specifies whether the given type should be given standard models.
     1.8 -Nonstandard models are unsound but can help debug inductive arguments,
     1.9 -as explained in \S\ref{inductive-properties}.
    1.10 +Specifies whether the given (recursive) datatype should be given standard
    1.11 +models. Nonstandard models are unsound but can help debug structural induction
    1.12 +proofs, as explained in \S\ref{inductive-properties}.
    1.13 +%This option is not supported for the type \textit{nat}.
    1.14  
    1.15  \optrue{std}{non\_std}
    1.16  Specifies the default standardness to use. This can be overridden on a per-type