# HG changeset patch
# User blanchet
# Date 1401106548 -7200
# Node ID 353652f479742cf17e4cc0f0dca5c9fbf3801aff
# Parent  c3f95255c7e5b9d217376d58afc0b6238b8ee4d8
renamed 'MaSh' option

diff -r c3f95255c7e5 -r 353652f47974 NEWS
--- 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
diff -r c3f95255c7e5 -r 353652f47974 src/Doc/Sledgehammer/document/root.tex
--- 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,
diff -r c3f95255c7e5 -r 353652f47974 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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
diff -r c3f95255c7e5 -r 353652f47974 src/HOL/Tools/etc/options
--- 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)"