# HG changeset patch
# User blanchet
# Date 1325511409 -3600
# Node ID 3ab55dfd2400958921c33155ab00c6b6d592ff3c
# Parent  b2594cc862d7100175745a2228cadac731393d9c
update docs to reflect "Manual_Nits"

diff -r b2594cc862d7 -r 3ab55dfd2400 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Jan 02 14:32:20 2012 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Jan 02 14:36:49 2012 +0100
@@ -910,7 +910,7 @@
 \prew
 \textbf{coinductive} \textit{nats} \textbf{where} \\
 ``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
-\textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
+\textbf{lemma} ``$\textit{nats} = (\lambda n.\; n \mathbin\in \{0, 1, 2, 3, 4\})$'' \\
 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
 \slshape Nitpick found a counterexample:
 \\[2\smallskipamount]