# HG changeset patch
# User blanchet
# Date 1391444318 -3600
# Node ID 30d874dc70008e0004cb5ca8332fb2c8e4f0174c
# Parent  1a4358d14ce252cb8c90a6f9e2bf4d28654c696d
added new option to documentation

diff -r 1a4358d14ce2 -r 30d874dc7000 NEWS
--- a/NEWS	Mon Feb 03 17:13:31 2014 +0100
+++ b/NEWS	Mon Feb 03 17:18:38 2014 +0100
@@ -115,6 +115,8 @@
   * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
 
 * Sledgehammer:
+  - New option:
+      smt
   - Renamed options:
       isar_compress ~> compress_isar
       isar_try0 ~> try0_isar
diff -r 1a4358d14ce2 -r 30d874dc7000 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:13:31 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:18:38 2014 +0100
@@ -1067,9 +1067,9 @@
 
 \opdefault{max\_facts}{smart\_int}{smart}
 Specifies the maximum number of facts that may be returned by the relevance
-filter. If the option is set to \textit{smart}, it is set to a value that was
-empirically found to be appropriate for the prover. Typical values range between
-50 and 1000.
+filter. If the option is set to \textit{smart}, it effectively takes a value
+that was empirically found to be appropriate for the prover. Typical values
+range between 50 and 1000.
 
 For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
 \textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
@@ -1093,7 +1093,7 @@
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_facts}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it is set to a value
+type encoding used. If the option is set to \textit{smart}, it takes a value
 that was empirically found to be appropriate for the prover. For most provers,
 this value is 100.
 
@@ -1104,7 +1104,7 @@
 Specifies the maximum number of iterations for the monomorphization fixpoint
 construction. The higher this limit is, the more monomorphic instances are
 potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it is set to a value
+type encoding used. If the option is set to \textit{smart}, it takes a value
 that was empirically found to be appropriate for the prover. For most provers,
 this value is 3.
 
@@ -1313,9 +1313,13 @@
 
 \optrue{try0\_isar}{dont\_try0\_isar}
 Specifies whether standard proof methods such as \textit{auto} and
-\textit{blast} should be tried as alternatives to \textit{metis} and
-\textit{smt} in Isar proofs. The collection of methods is roughly the same as
-for the \textbf{try0} command.
+\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
+The collection of methods is roughly the same as for the \textbf{try0} command.
+
+\opsmart{smt}{no\_smt}
+Specifies whether the \textit{smt} proof method should be tried as an
+alternative to \textit{metis}.  If the option is set to \textit{smart}, the
+\textit{smt} method is used for one-line proofs but not in Isar proofs.
 \end{enum}
 
 \subsection{Authentication}