--- a/doc-src/Nitpick/nitpick.tex Thu Oct 22 16:34:49 2009 +0200
+++ b/doc-src/Nitpick/nitpick.tex Fri Oct 23 14:45:01 2009 +0200
@@ -108,6 +108,10 @@
must find a model for the axioms. If it finds no model, we have an indication
that the axioms might be unsatisfiable.
+Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
+machine called \texttt{java}. The examples presented in this manual can be found
+in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
+
\newbox\boxA
\setbox\boxA=\hbox{\texttt{nospam}}
@@ -2474,7 +2478,7 @@
\item[$\bullet$] Local definitions are not supported and result in an error.
\item[$\bullet$] All constants and types whose names start with
-\textit{Nitpick}{.} or \textit{NitpickDefs}{.} are reserved for internal use.
+\textit{Nitpick}{.} are reserved for internal use.
\end{enum}
\let\em=\sl