# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 6c8170f8849e38b4465e057f91ffbc6f9c9c2d3b
# Parent  6ce09f69657c0e8805d7c6d5b7e85265bff5fd4c
don't mention "metisX" so much in the docs -- it will go away soon

diff -r 6ce09f69657c -r 6c8170f8849e doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 20:36:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 20:36:35 2011 +0200
@@ -492,33 +492,30 @@
 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 are metisFT and metisX?}
+\point{What is metisFT?}
 
 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 \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}).)
+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}).)
 
 If you see the warning
 
 \prew
 \slshape
-Metis: Falling back on ``\textit{metisX\/}''.
+Metis: Falling back on ``\textit{metisFT\/}''.
 \postw
 
 in a successful Metis proof, you can advantageously replace the \textit{metis}
-call with \textit{metisX}.
+call with \textit{metisFT}.
 
 \point{Are generated proofs minimal?}
 
@@ -901,7 +898,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{metisX}).
+back on \textit{metisFT}).
 
 \item[$\bullet$]
 \textbf{%