--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 07 10:28:04 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 07 11:25:01 2012 +0200
@@ -871,15 +871,15 @@
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
-directory that contains the \texttt{iprover} executable. Sledgehammer has been
-tested with version 0.99.
+directory that contains the \texttt{iprover} and \texttt{vclausify\_rel}
+executables. Sledgehammer has been tested with version 0.99.
\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an
instantiation-based prover with native support for equality developed by
Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use
iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the
-directory that contains the \texttt{iprover-eq} executable. Sledgehammer has
-been tested with version 0.8.
+directory that contains the \texttt{iprover-eq} and \texttt{vclausify\_rel}
+executables. Sledgehammer has been tested with version 0.8.
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},