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

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}