author blanchet Wed, 17 Mar 2010 16:11:48 +0100 changeset 35811 3939ca38f366 parent 35809 1ed86128316c child 35812 394fe2b064cd
minor additions to Nitpick docs
--- 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,