doc-src/Nitpick/nitpick.tex
changeset 35811 3939ca38f366
parent 35809 1ed86128316c
child 36126 00d550b6cfd4
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Wed Mar 17 12:21:54 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Wed Mar 17 16:11:48 2010 +0100
     1.3 @@ -2826,6 +2826,9 @@
     1.4  representation of functions synthesized by Isabelle, which is an implementation
     1.5  detail.
     1.6  
     1.7 +\item[$\bullet$] Axioms that restrict the possible values of the
     1.8 +\textit{undefined} constant are in general ignored.
     1.9 +
    1.10  \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
    1.11  which can become invalid if you change the definition of an inductive predicate
    1.12  that is registered in the cache. To clear the cache,