1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Mar 17 12:01:01 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Mar 17 12:21:54 2010 +0100
1.3 @@ -2617,6 +2617,12 @@
1.4 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
1.5 optional monotonic operator. The order of the assumptions is irrelevant.
1.6
1.7 +\flushitem{\textit{nitpick\_choice\_spec}}
1.8 +
1.9 +\nopagebreak
1.10 +This attribute specifies the (free-form) specification of a constant defined
1.11 +using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
1.12 +
1.13 \end{itemize}
1.14
1.15 When faced with a constant, Nitpick proceeds as follows:
1.16 @@ -2629,7 +2635,12 @@
1.17 the constant is not empty, it uses these rules as the specification of the
1.18 constant.
1.19
1.20 -\item[3.] Otherwise, it looks up the definition of the constant:
1.21 +\item[3.] Otherwise, if the constant was defined using the
1.22 +\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
1.23 +\textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
1.24 +uses these theorems as the specification of the constant.
1.25 +
1.26 +\item[4.] Otherwise, it looks up the definition of the constant:
1.27
1.28 \begin{enum}
1.29 \item[1.] If the \textit{nitpick\_def} set associated with the constant