# HG changeset patch
# User blanchet
# Date 1281085557 -7200
# Node ID d4cbc80e72713664882c38116b294a7f4919aa89
# Parent  a7e92239922f17030011de312778e4f97df0f313
extend the scope of limitation about nonconservative extensions

diff -r a7e92239922f -r d4cbc80e7271 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Fri Aug 06 10:50:52 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Fri Aug 06 11:05:57 2010 +0200
@@ -2864,16 +2864,19 @@
 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
 \postw
 
-Such theorems are considered bad style because they rely on the internal
-representation of functions synthesized by Isabelle, which is an implementation
+Such theorems are generally considered bad style because they rely on the
+internal representation of functions synthesized by Isabelle, 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.
+\item[$\bullet$] Axioms or definitions that restrict the possible values of the
+\textit{undefined} constant or other partially specified built-in Isabelle
+constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
+ignored. Again, such nonconservative extensions are generally considered bad
+style.
 
 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
 which can become invalid if you change the definition of an inductive predicate