# HG changeset patch
# User blanchet
# Date 1268824914 -3600
# Node ID 1ed86128316cbea8a18b77637e0549e7224789f9
# Parent  df56c1b1680fc72e39797f5422265ecf0dd5908b
document "nitpick_choice_spec" attribute

diff -r df56c1b1680f -r 1ed86128316c doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Wed Mar 17 12:01:01 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Mar 17 12:21:54 2010 +0100
@@ -2617,6 +2617,12 @@
 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
 optional monotonic operator. The order of the assumptions is irrelevant.
 
+\flushitem{\textit{nitpick\_choice\_spec}}
+
+\nopagebreak
+This attribute specifies the (free-form) specification of a constant defined
+using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
+
 \end{itemize}
 
 When faced with a constant, Nitpick proceeds as follows:
@@ -2629,7 +2635,12 @@
 the constant is not empty, it uses these rules as the specification of the
 constant.
 
-\item[3.] Otherwise, it looks up the definition of the constant:
+\item[3.] Otherwise, if the constant was defined using the
+\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
+\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:
 
 \begin{enum}
 \item[1.] If the \textit{nitpick\_def} set associated with the constant