renamed 'MaSh' option
authorblanchet
Mon May 26 14:15:48 2014 +0200 (2014-05-26)
changeset 57089353652f47974
parent 57088 c3f95255c7e5
child 57090 0224caba67ca
renamed 'MaSh' option
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/etc/options
     1.1 --- a/NEWS	Mon May 26 14:10:10 2014 +0200
     1.2 +++ b/NEWS	Mon May 26 14:15:48 2014 +0200
     1.3 @@ -381,9 +381,9 @@
     1.4  * Sledgehammer:
     1.5    - New prover "z3_new" with support for Isar proofs
     1.6    - MaSh overhaul:
     1.7 -      - A new SML-based learning engine eliminates the dependency on Python
     1.8 -        and increases performance and reliability.
     1.9 -      - Activation of MaSh now works via the "mash" system option (without
    1.10 +      - New SML-based learning engines eliminate the dependency on Python
    1.11 +        and increase performance and reliability.
    1.12 +      - Activation of MaSh now works via the "MaSh" system option (without
    1.13          requiring restart), instead of former settings variable "MASH".
    1.14          The option can be edited in Isabelle/jEdit menu Plugin
    1.15          Options / Isabelle / General. Allowed values include "sml" (for the
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Mon May 26 14:10:10 2014 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Mon May 26 14:15:48 2014 +0200
     2.3 @@ -1084,7 +1084,7 @@
     2.4  
     2.5  To enable MaSh, set the variable \texttt{MASH} to the name of the desired
     2.6  engine---either in the environment in which Isabelle is launched, in your
     2.7 -\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``Mash'' option
     2.8 +\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``MaSh'' option
     2.9  under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
    2.10  Persistent data for both engines is stored in the directory
    2.11  \texttt{\$ISABELLE\_HOME\_USER/mash}. When switching to the \textit{py} engine,
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 26 14:10:10 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 26 14:15:48 2014 +0200
     3.3 @@ -117,7 +117,7 @@
     3.4  datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
     3.5  
     3.6  fun mash_engine () =
     3.7 -  let val flag1 = Options.default_string @{system_option maSh} in
     3.8 +  let val flag1 = Options.default_string @{system_option MaSh} in
     3.9      (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
    3.10        "yes" => SOME MaSh_Py
    3.11      | "py" => SOME MaSh_Py
     4.1 --- a/src/HOL/Tools/etc/options	Mon May 26 14:10:10 2014 +0200
     4.2 +++ b/src/HOL/Tools/etc/options	Mon May 26 14:15:48 2014 +0200
     4.3 @@ -35,5 +35,5 @@
     4.4  public option z3_non_commercial : string = "unknown"
     4.5    -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     4.6  
     4.7 -public option maSh : string = "none"
     4.8 +public option MaSh : string = "none"
     4.9    -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)"