doc-src/Nitpick/nitpick.tex
changeset 33195 0efe26262e73
parent 33193 6f6baa3ef4dd
child 33196 5fe67e108651
--- 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