added new option to documentation
authorblanchet
Mon Feb 03 17:18:38 2014 +0100 (2014-02-03)
changeset 5528930d874dc7000
parent 55288 1a4358d14ce2
child 55290 3951ced4156c
added new option to documentation
NEWS
src/Doc/Sledgehammer/document/root.tex
     1.1 --- a/NEWS	Mon Feb 03 17:13:31 2014 +0100
     1.2 +++ b/NEWS	Mon Feb 03 17:18:38 2014 +0100
     1.3 @@ -115,6 +115,8 @@
     1.4    * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
     1.5  
     1.6  * Sledgehammer:
     1.7 +  - New option:
     1.8 +      smt
     1.9    - Renamed options:
    1.10        isar_compress ~> compress_isar
    1.11        isar_try0 ~> try0_isar
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:13:31 2014 +0100
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:18:38 2014 +0100
     2.3 @@ -1067,9 +1067,9 @@
     2.4  
     2.5  \opdefault{max\_facts}{smart\_int}{smart}
     2.6  Specifies the maximum number of facts that may be returned by the relevance
     2.7 -filter. If the option is set to \textit{smart}, it is set to a value that was
     2.8 -empirically found to be appropriate for the prover. Typical values range between
     2.9 -50 and 1000.
    2.10 +filter. If the option is set to \textit{smart}, it effectively takes a value
    2.11 +that was empirically found to be appropriate for the prover. Typical values
    2.12 +range between 50 and 1000.
    2.13  
    2.14  For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
    2.15  \textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
    2.16 @@ -1093,7 +1093,7 @@
    2.17  Specifies the maximum number of monomorphic instances to generate beyond
    2.18  \textit{max\_facts}. The higher this limit is, the more monomorphic instances
    2.19  are potentially generated. Whether monomorphization takes place depends on the
    2.20 -type encoding used. If the option is set to \textit{smart}, it is set to a value
    2.21 +type encoding used. If the option is set to \textit{smart}, it takes a value
    2.22  that was empirically found to be appropriate for the prover. For most provers,
    2.23  this value is 100.
    2.24  
    2.25 @@ -1104,7 +1104,7 @@
    2.26  Specifies the maximum number of iterations for the monomorphization fixpoint
    2.27  construction. The higher this limit is, the more monomorphic instances are
    2.28  potentially generated. Whether monomorphization takes place depends on the
    2.29 -type encoding used. If the option is set to \textit{smart}, it is set to a value
    2.30 +type encoding used. If the option is set to \textit{smart}, it takes a value
    2.31  that was empirically found to be appropriate for the prover. For most provers,
    2.32  this value is 3.
    2.33  
    2.34 @@ -1313,9 +1313,13 @@
    2.35  
    2.36  \optrue{try0\_isar}{dont\_try0\_isar}
    2.37  Specifies whether standard proof methods such as \textit{auto} and
    2.38 -\textit{blast} should be tried as alternatives to \textit{metis} and
    2.39 -\textit{smt} in Isar proofs. The collection of methods is roughly the same as
    2.40 -for the \textbf{try0} command.
    2.41 +\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
    2.42 +The collection of methods is roughly the same as for the \textbf{try0} command.
    2.43 +
    2.44 +\opsmart{smt}{no\_smt}
    2.45 +Specifies whether the \textit{smt} proof method should be tried as an
    2.46 +alternative to \textit{metis}.  If the option is set to \textit{smart}, the
    2.47 +\textit{smt} method is used for one-line proofs but not in Isar proofs.
    2.48  \end{enum}
    2.49  
    2.50  \subsection{Authentication}