# HG changeset patch # User blanchet # Date 1268838708 -3600 # Node ID 3939ca38f366bbfab329d068a50a32af129310c5 # Parent 1ed86128316cbea8a18b77637e0549e7224789f9 minor additions to Nitpick docs diff -r 1ed86128316c -r 3939ca38f366 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Wed Mar 17 12:21:54 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Mar 17 16:11:48 2010 +0100 @@ -2826,6 +2826,9 @@ representation of functions synthesized by Isabelle, which is an implementation detail. +\item[$\bullet$] Axioms that restrict the possible values of the +\textit{undefined} constant are in general ignored. + \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions, which can become invalid if you change the definition of an inductive predicate that is registered in the cache. To clear the cache,