diff -r 0debf65972c7 -r 122e67e77493 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 27 08:52:40 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 27 08:52:40 2012 +0200
@@ -909,8 +909,8 @@
 
 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
 an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
-formats (FOF and TFF0). It is included for experimental purposes. It
-requires version 3.0 or above. To use it, set the environment variable
+formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
+requires version 4.0 or above. To use it, set the environment variable
 \texttt{Z3\_HOME} to the directory that contains the \texttt{z3}
 executable.
 \end{enum}