# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 93d5aab90d8b6da8de4b60b99f9099c9eb06f63e
# Parent  09ad83de849c8888462a514ff765f32aed04f9c4
updated Sledgehammer docs

diff -r 09ad83de849c -r 93d5aab90d8b doc-src/Sledgehammer/sledgehammer.tex
--- 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}.