# HG changeset patch
# User blanchet
# Date 1404924517 -7200
# Node ID 5e8317c5b689b0c7c6edd8d70821e9f8bc83873c
# Parent  9b99b773acd4969f2c798e68d1d16a442ff40e3b
improved docs

diff -r 9b99b773acd4 -r 5e8317c5b689 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 09 11:54:01 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 09 18:48:37 2014 +0200
@@ -872,19 +872,12 @@
 the environment variable \texttt{LEO2\_HOME} to the directory that contains the
 \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
 
-\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
-the external provers, Metis itself can be used for proof search.
-
 \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). To use Satallax, set the
 environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
 \texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
 
-\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt2} proof method with the
-current settings (usually:\ Z3 with proof reconstruction) can be used for proof
-search.
-
 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
@@ -909,7 +902,6 @@
 via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
 > Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
 a pre-release version of 4.3.2.
-\end{enum}
 
 \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
@@ -917,10 +909,11 @@
 version 4.3.1 of Z3 or above. To use it, set the environment variable
 \texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
 executable.
+\end{enum}
 
 \end{sloppy}
 
-In addition to the local provers, the following remote provers are supported:
+Moreover, the following remote provers are supported:
 
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
@@ -980,6 +973,13 @@
 SPASS, and Vampire for 5~seconds yields a similar success rate to running the
 most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
 
+In addition to the local and remote provers, the Isabelle proof methods
+\textit{metis} and \textit{smt2} can be specified as \textbf{\textit{metis}}
+and \textbf{\textit{smt}}, respectively. They are generally not recommended
+for proof search but occasionally arise in Sledgehammer-generated
+minimization commands (e.g.,
+``\textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{metis}]'').
+
 For the \textit{min} subcommand, the default prover is \textit{metis}. If
 several provers are set, the first one is used.