doc-src/Nitpick/nitpick.tex
changeset 35185 9b8f351cced6
parent 35183 8580ba651489
child 35189 250fe9541fb2
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Wed Feb 17 11:20:09 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Wed Feb 17 12:14:08 2010 +0100
     1.3 @@ -472,7 +472,9 @@
     1.4  \prew
     1.5  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
     1.6  \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
     1.7 -\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
     1.8 +\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
     1.9 +fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
    1.10 +Nitpick found a potential counterexample: \\[2\smallskipamount]
    1.11  \hbox{}\qquad Free variable: \nopagebreak \\
    1.12  \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
    1.13  Confirmation by ``\textit{auto}'': The above counterexample is genuine.