1.1 --- a/doc-src/Nitpick/nitpick.tex	Sat Apr 24 17:48:21 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sun Apr 25 00:10:30 2010 +0200
     1.3 @@ -428,9 +428,6 @@
     1.4  $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
     1.5  from \textit{sym}'s definition.
     1.6  
     1.7 -Although skolemization is a useful optimization, you can disable it by invoking
     1.8 -Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
     1.9 -
    1.10  \subsection{Natural Numbers and Integers}
    1.11  \label{natural-numbers-and-integers}
    1.12  
    1.13 @@ -2199,9 +2196,6 @@
    1.14  formula and usually help us to understand why the counterexample falsifies the
    1.15  formula.
    1.16  
    1.17 -\nopagebreak
    1.18 -{\small See also \textit{skolemize} (\S\ref{optimizations}).}
    1.19 -
    1.20  \opfalse{show\_datatypes}{hide\_datatypes}
    1.21  Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
    1.22  be displayed as part of counterexamples. Such subsets are sometimes helpful when
    1.23 @@ -2451,15 +2445,6 @@
    1.24  {\small See also \textit{debug} (\S\ref{output-format}) and
    1.25  \textit{show\_consts} (\S\ref{output-format}).}
    1.26  
    1.27 -\optrue{skolemize}{dont\_skolemize}
    1.28 -Specifies whether the formula should be skolemized. For performance reasons,
    1.29 -(positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
    1.30 -(positive) $\exists$-quanti\-fier are left unchanged.
    1.31 -
    1.32 -\nopagebreak
    1.33 -{\small See also \textit{debug} (\S\ref{output-format}) and
    1.34 -\textit{show\_skolems} (\S\ref{output-format}).}
    1.35 -
    1.36  \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
    1.37  Specifies whether Nitpick should use Kodkod's transitive closure operator to
    1.38  encode non-well-founded ``linear inductive predicates,'' i.e., inductive