1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Aug 03 12:31:30 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Aug 03 13:17:15 2010 +0200
     1.3 @@ -2602,7 +2602,6 @@
     1.4  \nopagebreak
     1.5  This attribute specifies the (free-form) specification of a constant defined
     1.6  using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
     1.7 -
     1.8  \end{enum}
     1.9  
    1.10  When faced with a constant, Nitpick proceeds as follows:
    1.11 @@ -2660,6 +2659,22 @@
    1.12  \textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
    1.13  \postw
    1.14  
    1.15 +Moreover, because of its internal three-valued logic, Nitpick tends to lose a
    1.16 +lot of precision in the presence of partially specified constants. For example,
    1.17 +
    1.18 +\prew
    1.19 +\textbf{lemma} $\mathit{list\_of\_LCons}$ [\textit{nitpick\_simp}]: \\
    1.20 +``$\textit{list\_of}~(\textit{LCons~x~xs}) = {}$ \\
    1.21 +\phantom{``}$(\textrm{if}~\textit{lfinite~xs}~\textrm{then}~x \mathbin{\#} \textit{list\_of~xs}~\textrm{else}~\textit{undefined})$''
    1.22 +\postw
    1.23 +
    1.24 +is superior to
    1.25 +
    1.26 +\prew
    1.27 +\textbf{lemma} $\mathit{list\_of\_LCons}$ [\textit{nitpick\_psimp}]: \\
    1.28 +``$\textit{lfinite~xs} \,\Longrightarrow\, \textit{list\_of}~(\textit{LCons~x~xs}) = x \mathbin{\#} \textit{list\_of~xs\/}$''
    1.29 +\postw
    1.30 +
    1.31  Such tweaks should be done with great care, because Nitpick will assume that the
    1.32  constant is completely defined by its equational specification. For example, if
    1.33  you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define