1.1 --- a/doc-src/Nitpick/nitpick.tex	Fri Aug 06 10:50:52 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Aug 06 11:05:57 2010 +0200
     1.3 @@ -2864,16 +2864,19 @@
     1.4  \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
     1.5  \postw
     1.6  
     1.7 -Such theorems are considered bad style because they rely on the internal
     1.8 -representation of functions synthesized by Isabelle, which is an implementation
     1.9 +Such theorems are generally considered bad style because they rely on the
    1.10 +internal representation of functions synthesized by Isabelle, an implementation
    1.11  detail.
    1.12  
    1.13  \item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
    1.14  theorems that rely on the use of the indefinite description operator internally
    1.15  by \textbf{specification} and \textbf{quot\_type}.
    1.16  
    1.17 -\item[$\bullet$] Axioms that restrict the possible values of the
    1.18 -\textit{undefined} constant are in general ignored.
    1.19 +\item[$\bullet$] Axioms or definitions that restrict the possible values of the
    1.20 +\textit{undefined} constant or other partially specified built-in Isabelle
    1.21 +constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
    1.22 +ignored. Again, such nonconservative extensions are generally considered bad
    1.23 +style.
    1.24  
    1.25  \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
    1.26  which can become invalid if you change the definition of an inductive predicate