--- a/doc-src/Sledgehammer/sledgehammer.tex Sat Oct 29 13:15:58 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Oct 29 13:15:58 2011 +0200
@@ -724,7 +724,8 @@
\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP many-typed higher-order syntax (THF0).
+with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
+requires version 1.2.9 or above.
\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
the external provers, Metis itself can be used for proof search.