# HG changeset patch
# User blanchet
# Date 1281010834 -7200
# Node ID 39e84a503840a469bfda6c46c900d85960e442db
# Parent  379fb08da97be3d89b3ff8d9950f4875185be36c
more docs

diff -r 379fb08da97b -r 39e84a503840 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Aug 05 14:10:18 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Thu Aug 05 14:20:34 2010 +0200
@@ -2581,9 +2581,9 @@
 
 \nopagebreak
 This attribute specifies the equations that constitute the specification of a
-constant. For functions defined using the \textbf{primrec}, \textbf{function},
-and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
-\textit{simps} rules. The equations must be of the form
+constant. The \textbf{primrec}, \textbf{function}, and
+\textbf{nominal\_\allowbreak primrec} packages automatically attach this
+attribute to their \textit{simps} rules. The equations must be of the form
 
 \qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr]$
 
@@ -2595,9 +2595,9 @@
 
 \nopagebreak
 This attribute specifies the equations that constitute the partial specification
-of a constant. For functions defined using the \textbf{function} package, this
-corresponds to the \textit{psimps} rules. The conditional equations must be of
-the form
+of a constant. The \textbf{function} package automatically attaches this
+attribute to its \textit{psimps} rules. The conditional equations must be of the
+form
 
 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$
 
@@ -2627,15 +2627,13 @@
 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
 uses these theorems as the specification of the constant.
 
-\item[4.] Otherwise, it looks up the definition of the constant:
+\item[4.] Otherwise, it looks up the definition of the constant. If the
+\textit{nitpick\_def} set associated with the constant is not empty, it uses the
+latest rule added to the set as the definition of the constant; otherwise it
+uses the actual definition axiom.
 
 \begin{enum}
-\item[1.] If the \textit{nitpick\_def} set associated with the constant is not
-empty, it uses the latest rule added to the set as the definition of the
-constant; otherwise it uses the actual definition axiom. In addition, the
-constant is \textsl{unfolded} wherever it appears (as opposed to defined
-equationally).
-\item[2.] If the definition is of the form
+\item[1.] If the definition is of the form
 
 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$
 
@@ -2648,6 +2646,10 @@
 \textit{Spec\_Rules} table. The tool uses the introduction rules to ascertain
 whether the definition is well-founded and the definition to generate a
 fixed-point equation or an unrolled equation.
+
+\item[2.] If the definition is compact enough, the constant is \textsl{unfolded}
+wherever it appears; otherwise, it is defined equationally, as with
+the \textit{nitpick\_simp} attribute.
 \end{enum}
 \end{enum}
 
@@ -2696,8 +2698,9 @@
 ``$\lnot\, \textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{True\/}$''
 \postw
 
-Because Nitpick unfolds definitions but not simplification rules, it often pays
-off to declare long-winded definitions as \textit{nitpick\_simp}. For example:
+Because Nitpick sometimes unfolds definitions but never simplification rules,
+you can ensure that a constant is defined explicitly using the
+\textit{nitpick\_simp}. For example:
 
 \prew
 \textbf{definition}~\textit{optimum} \textbf{where} [\textit{nitpick\_simp}]: \\