# HG changeset patch
# User blanchet
# Date 1403090589 -7200
# Node ID fd539459a112ff9f585f569db1679aa791079bb2
# Parent  3a20f8a24b13fc4c126859901a8c75db5b2dc7aa
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable

diff -r 3a20f8a24b13 -r fd539459a112 NEWS
--- a/NEWS	Tue Jun 17 18:41:44 2014 +0200
+++ b/NEWS	Wed Jun 18 13:23:09 2014 +0200
@@ -392,11 +392,11 @@
   - MaSh overhaul:
       - New SML-based learning engines eliminate the dependency on Python
         and increase performance and reliability.
-      - Activation of MaSh now works via the "MaSh" system option (without
-        requiring restart), instead of former settings variable "MASH".
-        The option can be edited in Isabelle/jEdit menu Plugin
-        Options / Isabelle / General. Allowed values include "sml" (for the
-        default SML engine), "py" (for the old Python engine), and "none".
+      - MaSh and MeSh are now used by default together with the traditional
+        MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
+        system option in Plugin Options / Isabelle / General to "none". Other
+        allowed values include "sml" (for the default SML engine) and "py"
+        (for the old Python engine).
   - New option:
       smt_proofs
   - Renamed options:
diff -r 3a20f8a24b13 -r fd539459a112 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Jun 17 18:41:44 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jun 18 13:23:09 2014 +0200
@@ -395,9 +395,9 @@
 and it cannot learn.
 
 \item[\labelitemi]
-An experimental alternative to MePo is \emph{MaSh}
-(\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It
-applies machine learning to the problem of finding relevant facts.
+An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for
+\underline{S}ledge\underline{h}ammer). It applies machine learning to the
+problem of finding relevant facts.
 
 \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
 \end{enum}
@@ -1056,7 +1056,7 @@
 The traditional memoryless MePo relevance filter.
 
 \item[\labelitemi] \textbf{\textit{mash}:}
-The experimental MaSh machine learner. Three learning engines are provided:
+The MaSh machine learner. Three learning engines are provided:
 
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{sml\_nb}} (also called \textbf{\textit{sml}}
@@ -1069,6 +1069,9 @@
 The program is included with Isabelle as \texttt{mash.py}.
 \end{enum}
 
+In addition, the special value \textit{none} is used to disable machine learning by
+default (cf.\ \textit{smart} below).
+
 The engine can be selected by setting \texttt{MASH} to the name of the desired
 engine---either in the environment in which Isabelle is launched, in your
 \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``MaSh'' option
@@ -1083,15 +1086,10 @@
 rankings from MePo and MaSh.
 
 \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
-MeSh if MaSh is a learning engine has been specified (as explained above);
-otherwise, MePo.
+MeSh. If the learning engine is set to be \textit{none}, \textit{smart} behaves
+like MePo.
 \end{enum}
 
-The behavior of \textit{smart} ensures that MaSh is not used by default,
-reflecting the experimental nature of the filter. Nevertheless, there is ample
-empirical evidence in favor of a combination of MePo, MaSh, and MeSh, and you
-are warmly encouraged to try it out.
-
 \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} (the default), it effectively
diff -r 3a20f8a24b13 -r fd539459a112 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Tue Jun 17 18:41:44 2014 +0200
+++ b/src/HOL/Tools/etc/options	Wed Jun 18 13:23:09 2014 +0200
@@ -35,5 +35,5 @@
 public option z3_non_commercial : string = "unknown"
   -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
 
-public option MaSh : string = "none"
+public option MaSh : string = "sml"
   -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)"