doc-src/Nitpick/nitpick.tex

 
 \nopagebreak
 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
 \textit{batch\_size} (\S\ref{optimizations}).}
 
-\optrue{show\_skolems}{hide\_skolem}
-Specifies whether the values of Skolem constants should be displayed as part of
-counterexamples. Skolem constants correspond to bound variables in the original
-formula and usually help us to understand why the counterexample falsifies the
-formula.
-
 \opfalse{show\_datatypes}{hide\_datatypes}
 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
 be displayed as part of counterexamples. Such subsets are sometimes helpful when
 investigating whether a potential counterexample is genuine or spurious, but
 their potential for clutter is real.

 its axioms) should be displayed along with any counterexample. These values are
 sometimes helpful when investigating why a counterexample is
 genuine, but they can clutter the output.
 
 \opfalse{show\_all}{dont\_show\_all}
-Enabling this option effectively enables \textit{show\_skolems},
-\textit{show\_datatypes}, and \textit{show\_consts}.
+Enabling this option effectively enables \textit{show\_datatypes} and
+\textit{show\_consts}.
 
 \opdefault{max\_potential}{int}{$\mathbf{1}$}
 Specifies the maximum number of potential counterexamples to display. Setting
 this option to 0 speeds up the search for a genuine counterexample. This option
 is implicitly set to 0 for automatic runs. If you set this option to a value