# HG changeset patch
# User blanchet
# Date 1298285438 -3600
# Node ID afd7405f1d7ec0434d25d7de032e614f70b5e148
# Parent  79a79460b70cf160822c743b579256f725588cd6
updated docs w.r.t. "nitpick_unfold" attribute

diff -r 79a79460b70c -r afd7405f1d7e doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:38 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:38 2011 +0100
@@ -2536,12 +2536,12 @@
 following attributes to affect Nitpick's behavior:
 
 \begin{enum}
-\flushitem{\textit{nitpick\_def}}
+\flushitem{\textit{nitpick\_unfold}}
 
 \nopagebreak
-This attribute specifies an alternative definition of a constant. The
-alternative definition should be logically equivalent to the constant's actual
-axiomatic definition and should be of the form
+This attribute specifies an equation that Nitpick should use to expand a
+constant. The equation should be logically equivalent to the constant's actual
+definition and should be of the form
 
 \qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$,
 
@@ -2550,7 +2550,8 @@
 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
 
 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
-$t$.
+$t$. Each occurrence of $c$ in the problem is expanded to $\lambda x_1\,\ldots
+x_n.\; t$.
 
 \flushitem{\textit{nitpick\_simp}}
 
@@ -2603,8 +2604,8 @@
 uses these theorems as the specification 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
+\textit{nitpick\_unfold} 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}
@@ -2641,7 +2642,7 @@
 definition as follows:
 
 \prew
-\textbf{lemma} $\mathit{odd\_alt\_def}$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_alt\_unfold}$ [\textit{nitpick\_unfold}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
 \postw
 
 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
@@ -2691,7 +2692,7 @@
 and let Nitpick know about it:
 
 \prew
-\textbf{lemma} \textit{c\_alt\_def} [\textit{nitpick\_def}]:\kern.4em ``$c \equiv c'$\kern2pt ''
+\textbf{lemma} \textit{c\_alt\_unfold} [\textit{nitpick\_unfold}]:\kern.4em ``$c \equiv c'$\kern2pt ''
 \postw
 
 This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive