--- a/NEWS Mon May 26 14:10:10 2014 +0200
+++ b/NEWS Mon May 26 14:15:48 2014 +0200
@@ -381,9 +381,9 @@
* Sledgehammer:
- New prover "z3_new" with support for Isar proofs
- MaSh overhaul:
- - A new SML-based learning engine eliminates the dependency on Python
- and increases performance and reliability.
- - Activation of MaSh now works via the "mash" system option (without
+ - 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
--- a/src/Doc/Sledgehammer/document/root.tex Mon May 26 14:10:10 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Mon May 26 14:15:48 2014 +0200
@@ -1084,7 +1084,7 @@
To enable MaSh, set the variable \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
+\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``MaSh'' option
under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
Persistent data for both engines is stored in the directory
\texttt{\$ISABELLE\_HOME\_USER/mash}. When switching to the \textit{py} engine,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 26 14:10:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 26 14:15:48 2014 +0200
@@ -117,7 +117,7 @@
datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
fun mash_engine () =
- let val flag1 = Options.default_string @{system_option maSh} in
+ let val flag1 = Options.default_string @{system_option MaSh} in
(case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
"yes" => SOME MaSh_Py
| "py" => SOME MaSh_Py
--- a/src/HOL/Tools/etc/options Mon May 26 14:10:10 2014 +0200
+++ b/src/HOL/Tools/etc/options Mon May 26 14:15:48 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 = "none"
-- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)"