updated Nitpick's documentation w.r.t. finitization

--- a/doc-src/Nitpick/nitpick.tex	Tue Dec 07 11:56:53 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Dec 07 11:56:56 2010 +0100
@@ -2108,14 +2108,9 @@
 per-type basis using the \textit{box}~\qty{type} option described above.
 
 \opargboolorsmart{finitize}{type}{dont\_finitize}
-Specifies whether Nitpick should attempt to finitize a given type, which can be
-a function type or an infinite ``shallow datatype'' (an infinite datatype whose
-constructors don't appear in the problem).
-
-For function types, Nitpick performs a monotonicity analysis to detect functions
-that are constant at all but finitely many points (e.g., finite sets) and treats
-such occurrences specially, thereby increasing the precision. The option can
-then take the following values:
+Specifies whether Nitpick should attempt to finitize an infinite ``shallow
+datatype'' (an infinite datatype whose constructors don't appear in the
+problem). The option can then take the following values:
 
 \begin{enum}
 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
@@ -2132,12 +2127,9 @@
 genuine.''
 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
 \item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
-detect whether the datatype can be safely finitized before finitizing it.
+detect whether the datatype can be soundly finitized before finitizing it.
 \end{enum}
 
-Like other drastic optimizations, finitization can sometimes prevent the
-discovery of counterexamples.
-
 \nopagebreak
 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
 (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and