--- a/doc-src/Nitpick/nitpick.tex Wed Feb 17 10:28:37 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Feb 17 11:19:48 2010 +0100
@@ -1369,7 +1369,7 @@
\prew
\slshape
Hint: To check that the induction hypothesis is general enough, try this command:
-\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_all}].
+\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
\postw
If we follow the hint, we get a ``nonstandard'' counterexample for the step:
@@ -1397,11 +1397,10 @@
\postw
Reading the Nitpick manual is a most excellent idea.
-But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
-option told the tool to look for nonstandard models of binary trees, which
-means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
-addition to the standard trees generated by the \textit{Leaf} and
-\textit{Branch} constructors.%
+But what's going on? The \textit{non\_std} option told the tool to look for
+nonstandard models of binary trees, which means that new ``nonstandard'' trees
+$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
+generated by the \textit{Leaf} and \textit{Branch} constructors.%
\footnote{Notice the similarity between allowing nonstandard trees here and
allowing unreachable states in the preceding example (by removing the ``$n \in
\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the