1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -740,7 +740,7 @@
     1.4  
     1.5  \prew
     1.6  \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
     1.7 -\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount]
     1.8 +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
     1.9  \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
    1.10  Nitpick can compute it efficiently. \\[2\smallskipamount]
    1.11  Trying 1 scope: \\
    1.12 @@ -758,7 +758,7 @@
    1.13  
    1.14  \prew
    1.15  \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
    1.16 -\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount]
    1.17 +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
    1.18  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    1.19  \hbox{}\qquad Empty assignment
    1.20  \postw
    1.21 @@ -1752,7 +1752,7 @@
    1.22  
    1.23  \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
    1.24  problems that refer to the types \textit{rat} or \textit{real} or the constants
    1.25 -\textit{gcd} or \textit{lcm}.
    1.26 +\textit{Suc}, \textit{gcd}, or \textit{lcm}.
    1.27  
    1.28  {\small See also \textit{bits} (\S\ref{scope-of-search}) and
    1.29  \textit{show\_datatypes} (\S\ref{output-format}).}