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