# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID da6f459a70215fe8d0248a33170337f6828e1c37
# Parent  8d6a4978cc65b706ca0d7a06ba25ac12acd8c24c
imported patch sledge_doc_metis_as_prover

diff -r 8d6a4978cc65 -r da6f459a7021 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon May 30 17:00:38 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon May 30 17:00:38 2011 +0200
@@ -750,6 +750,11 @@
 \item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
 ATP, exploiting Z3's undocumented support for the TPTP format. It is included
 for experimental purposes. It requires version 2.18 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.
+
+\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
 \end{enum}
 
 In addition, the following remote provers are supported:
@@ -814,6 +819,9 @@
 success rate to running the most effective of these for 120~seconds
 \cite{boehme-nipkow-2010}.
 
+For the \textit{min} subcommand, the default prover is \textit{metis}. If
+several provers are set, the first one is used.
+
 \opnodefault{prover}{string}
 Alias for \textit{provers}.