--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Nov 18 11:47:12 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Nov 18 11:47:12 2011 +0100
@@ -750,19 +750,13 @@
\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
the external provers, Metis itself can be used for proof search.
-\item[\labelitemi] \textbf{\textit{metis\_full\_types}:} Fully typed version of
-Metis, corresponding to \textit{metis} (\textit{full\_types}).
-
-\item[\labelitemi] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
-corresponding to \textit{metis} (\textit{no\_types}).
-
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
support for the TPTP typed higher-order syntax (THF0). Sledgehammer
requires version 2.2 or above.
\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
-current settings (typically, Z3 with proof reconstruction).
+current settings (usually:\ Z3 with proof reconstruction).
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.