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