1.1 --- a/NEWS	Tue Jun 17 18:41:44 2014 +0200
     1.2 +++ b/NEWS	Wed Jun 18 13:23:09 2014 +0200
     1.3 @@ -392,11 +392,11 @@
     1.4    - MaSh overhaul:
     1.5        - New SML-based learning engines eliminate the dependency on Python
     1.6          and increase performance and reliability.
     1.7 -      - Activation of MaSh now works via the "MaSh" system option (without
     1.8 -        requiring restart), instead of former settings variable "MASH".
     1.9 -        The option can be edited in Isabelle/jEdit menu Plugin
    1.10 -        Options / Isabelle / General. Allowed values include "sml" (for the
    1.11 -        default SML engine), "py" (for the old Python engine), and "none".
    1.12 +      - MaSh and MeSh are now used by default together with the traditional
    1.13 +        MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
    1.14 +        system option in Plugin Options / Isabelle / General to "none". Other
    1.15 +        allowed values include "sml" (for the default SML engine) and "py"
    1.16 +        (for the old Python engine).
    1.17    - New option:
    1.18        smt_proofs
    1.19    - Renamed options:

     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue Jun 17 18:41:44 2014 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jun 18 13:23:09 2014 +0200
     2.3 @@ -395,9 +395,9 @@
     2.4  and it cannot learn.
     2.5  
     2.6  \item[\labelitemi]
     2.7 -An experimental alternative to MePo is \emph{MaSh}
     2.8 -(\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It
     2.9 -applies machine learning to the problem of finding relevant facts.
    2.10 +An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for
    2.11 +\underline{S}ledge\underline{h}ammer). It applies machine learning to the
    2.12 +problem of finding relevant facts.
    2.13  
    2.14  \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
    2.15  \end{enum}
    2.16 @@ -1056,7 +1056,7 @@
    2.17  The traditional memoryless MePo relevance filter.
    2.18  
    2.19  \item[\labelitemi] \textbf{\textit{mash}:}
    2.20 -The experimental MaSh machine learner. Three learning engines are provided:
    2.21 +The MaSh machine learner. Three learning engines are provided:
    2.22  
    2.23  \begin{enum}
    2.24  \item[\labelitemi] \textbf{\textit{sml\_nb}} (also called \textbf{\textit{sml}}
    2.25 @@ -1069,6 +1069,9 @@
    2.26  The program is included with Isabelle as \texttt{mash.py}.
    2.27  \end{enum}
    2.28  
    2.29 +In addition, the special value \textit{none} is used to disable machine learning by
    2.30 +default (cf.\ \textit{smart} below).
    2.31 +
    2.32  The engine can be selected by setting \texttt{MASH} to the name of the desired
    2.33  engine---either in the environment in which Isabelle is launched, in your
    2.34  \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``MaSh'' option
    2.35 @@ -1083,15 +1086,10 @@
    2.36  rankings from MePo and MaSh.
    2.37  
    2.38  \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
    2.39 -MeSh if MaSh is a learning engine has been specified (as explained above);
    2.40 -otherwise, MePo.
    2.41 +MeSh. If the learning engine is set to be \textit{none}, \textit{smart} behaves
    2.42 +like MePo.
    2.43  \end{enum}
    2.44  
    2.45 -The behavior of \textit{smart} ensures that MaSh is not used by default,
    2.46 -reflecting the experimental nature of the filter. Nevertheless, there is ample
    2.47 -empirical evidence in favor of a combination of MePo, MaSh, and MeSh, and you
    2.48 -are warmly encouraged to try it out.
    2.49 -
    2.50  \opdefault{max\_facts}{smart\_int}{smart}
    2.51  Specifies the maximum number of facts that may be returned by the relevance
    2.52  filter. If the option is set to \textit{smart} (the default), it effectively

     3.1 --- a/src/HOL/Tools/etc/options	Tue Jun 17 18:41:44 2014 +0200
     3.2 +++ b/src/HOL/Tools/etc/options	Wed Jun 18 13:23:09 2014 +0200
     3.3 @@ -35,5 +35,5 @@
     3.4  public option z3_non_commercial : string = "unknown"
     3.5    -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     3.6  
     3.7 -public option MaSh : string = "none"
     3.8 +public option MaSh : string = "sml"
     3.9    -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)"