author blanchet Wed, 17 Mar 2010 12:21:54 +0100 changeset 35809 1ed86128316c parent 35808 df56c1b1680f child 35810 a50237ec0ecd child 35811 3939ca38f366
document "nitpick_choice_spec" attribute
--- 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