# HG changeset patch
# User blanchet
# Date 1256301901 -7200
# Node ID 0efe26262e7315e1778959212c5a4637738415d9
# Parent  13450310a776c43f3b7b4fa71d9ba9a9742a521e
updated Nitpick manual to reflect the latest Stand der Dinge

diff -r 13450310a776 -r 0efe26262e73 doc-src/Nitpick/nitpick.tex
--- 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