# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 3f740034b927c1908241066c1cd1de447f45b315
# Parent  b02749a3b0acfd2eb61a0b148b503e0065221816
temporarily document "metisX"

diff -r b02749a3b0ac -r 3f740034b927 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 20:36:34 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 20:36:35 2011 +0200
@@ -492,30 +492,33 @@
 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
-\point{What is metisFT?}
+\point{What are metisFT and metisX?}
 
 The \textit{metisFT} proof method is the fully-typed version of Metis. It is
 much slower than \textit{metis}, but the proof search is fully typed, and it
 also includes more powerful rules such as the axiom ``$x = \mathit{True}
 \mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
-in set comprehensions). The method kicks in automatically as a fallback when
-\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
-\textit{metis} if the proof obviously requires type information or if
-\textit{metis} failed when Sledgehammer preplayed the proof. (By default,
-Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds
-to ensure that the generated one-line proofs actually work and to display timing
-information. This can be configured using the \textit{preplay\_timeout} option
-(\S\ref{timeouts}).)
+in set comprehensions).
+
+The \textit{metisX} proof method is an experimental version of Metis designed to
+subsume both \textit{metis} and \textit{metisFT}. The method kicks in
+automatically as a fallback when \textit{metis} fails, and it is sometimes
+generated by Sledgehammer instead of \textit{metis} if the proof obviously
+requires type information or if \textit{metis} failed when Sledgehammer
+preplayed the proof. (By default, Sledgehammer tries to run \textit{metis}
+and/or \textit{metisX} for 4 seconds to ensure that the generated one-line
+proofs actually work and to display timing information. This can be configured
+using the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
 
 If you see the warning
 
 \prew
 \slshape
-Metis: Falling back on ``\textit{metisFT\/}''.
+Metis: Falling back on ``\textit{metisX\/}''.
 \postw
 
 in a successful Metis proof, you can advantageously replace the \textit{metis}
-call with \textit{metisFT}.
+call with \textit{metisX}.
 
 \point{Are generated proofs minimal?}
 
@@ -751,6 +754,9 @@
 the external provers, Metis itself can be used for proof search.
 
 \item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
+
+\item[$\bullet$] \textbf{\textit{metisX}:} New experimental version of Metis,
+designed to subsume both \textit{metis} and \textit{metisFT}.
 \end{enum}
 
 In addition, the following remote provers are supported:
@@ -895,7 +901,7 @@
 Like for \textit{poly\_preds} constants are annotated with their types to
 resolve overloading, but otherwise no type information is encoded. This
 coincides with the encoding used by the \textit{metis} command (before it falls
-back on \textit{metisFT}).
+back on \textit{metisX}).
 
 \item[$\bullet$]
 \textbf{%