# HG changeset patch
# User blanchet
# Date 1290637044 -3600
# Node ID 3a10ce7cd436878500c16a0bec5d66985257abd6
# Parent  a961ec75fc29931bcc9d7b33adf88c0ab6d3fcde
document requirement on theory import

diff -r a961ec75fc29 -r 3a10ce7cd436 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Wed Nov 24 19:15:00 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Nov 24 23:17:24 2010 +0100
@@ -10,7 +10,7 @@
 \usepackage{multicol}
 \usepackage{stmaryrd}
 %\usepackage[scaled=.85]{beramono}
-\usepackage{../iman,../pdfsetup}
+\usepackage{../isabelle,../iman,../pdfsetup}
 
 %\oddsidemargin=4.6mm
 %\evensidemargin=4.6mm
@@ -117,8 +117,9 @@
 arguments in the theory text.
 
 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.
+machine called \texttt{java}. To run Nitpick, you must also make sure that the
+theory \textit{Nitpick} is imported---this is rarely a problem in practice
+since it is part of \textit{Main}.
 
 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
 Nitpick also provides an automatic mode that can be enabled via the ``Auto
@@ -129,6 +130,8 @@
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
+The examples presented in this manual can be found
+in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory.
 The known bugs and limitations at the time of writing are listed in
 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
 or this manual should be directed to
diff -r a961ec75fc29 -r 3a10ce7cd436 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 24 19:15:00 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 24 23:17:24 2010 +0100
@@ -10,7 +10,7 @@
 \usepackage{multicol}
 \usepackage{stmaryrd}
 %\usepackage[scaled=.85]{beramono}
-\usepackage{../iman,../pdfsetup}
+\usepackage{../isabelle,../iman,../pdfsetup}
 
 %\oddsidemargin=4.6mm
 %\evensidemargin=4.6mm
@@ -109,7 +109,9 @@
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
-Examples of Sledgehammer use can be found in Isabelle's
+To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
+imported---this is rarely a problem in practice since it is part of
+\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
 \texttt{src/HOL/Metis\_Examples} directory.
 Comments and bug reports concerning Sledgehammer or this manual should be
 directed to