--- a/doc-src/Nitpick/nitpick.tex Thu Aug 05 15:44:54 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Thu Aug 05 18:00:50 2010 +0200
@@ -2860,6 +2860,10 @@
representation of functions synthesized by Isabelle, which is an implementation
detail.
+\item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
+theorems that rely on the use of the indefinite description operator internally
+by \textbf{specification} and \textbf{quot\_type}.
+
\item[$\bullet$] Axioms that restrict the possible values of the
\textit{undefined} constant are in general ignored.