author blanchet Wed, 30 Sep 2015 13:58:46 +0200 changeset 61283 ed54b0531e9c parent 61282 3e578ddef85d child 61285 112effc2d580
updated docs
--- 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}