# HG changeset patch
# User blanchet
# Date 1344331501 -7200
# Node ID 56b633faec9934c6766555a304b67bc8a917f6fd
# Parent  d408ff0abf2381527534bf0d1217054e7940f0f6
documentation

diff -r d408ff0abf23 -r 56b633faec99 doc-src/Sledgehammer/sledgehammer.tex
--- 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},