--- a/src/Doc/Sledgehammer/document/root.tex Wed Sep 30 16:36:42 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Sep 30 16:40:17 2015 +0100
@@ -278,7 +278,7 @@
provers might be missing or present with a \textit{remote\_} prefix.
For each successful prover, Sledgehammer gives a one-line \textit{metis} or
-\textit{smt2} method call. Rough timings are shown in parentheses, indicating how
+\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
In addition, you can ask Sledgehammer for an Isar text proof by enabling the
@@ -289,7 +289,7 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt2} one-line
+readable and also faster than the \textit{metis} or \textit{smt} one-line
proofs. This feature is experimental and is only available for ATPs.
\section{Hints}
@@ -341,7 +341,7 @@
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
that Isar proofs should be generated, in addition to one-line \textit{metis} or
-\textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
+\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{compress} (\S\ref{output-format}).
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
@@ -1277,9 +1277,9 @@
The collection of methods is roughly the same as for the \textbf{try0} command.
\opsmart{smt\_proofs}{no\_smt\_proofs}
-Specifies whether the \textit{smt2} proof method should be tried in addition to
+Specifies whether the \textit{smt} proof method should be tried in addition to
Isabelle's other proof methods. If the option is set to \textit{smart} (the
-default), the \textit{smt2} method is used for one-line proofs but not in Isar
+default), the \textit{smt} method is used for one-line proofs but not in Isar
proofs.
\end{enum}