# HG changeset patch
# User blanchet
# Date 1443614326 -7200
# Node ID ed54b0531e9c364bf70d5300ac04e278cdcdfdd4
# Parent  3e578ddef85d015cb0330a69e66c5af0e12514b3
updated docs

diff -r 3e578ddef85d -r ed54b0531e9c src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Sep 29 23:43:35 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Sep 30 13:58:46 2015 +0200
@@ -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}