summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson <lp15@cam.ac.uk> |

Wed, 30 Sep 2015 16:40:17 +0100 | |

changeset 61285 | 112effc2d580 |

parent 61284 | 2314c2f62eb1 (current diff) |

parent 61283 | ed54b0531e9c (diff) |

child 61287 | 2f61e05ec124 |

Merge

--- 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}