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