# HG changeset patch # User blanchet # Date 1406220398 -7200 # Node ID b246943b3aa33ac09c1e9b72527c585ee1c23fb9 # Parent f55c173a3cbcdffa40d7e0d66c5d58c439b416f5 reenabled MaSh for Isabelle2014 release (hopefully) diff -r f55c173a3cbc -r b246943b3aa3 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Jul 24 18:46:38 2014 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jul 24 18:46:38 2014 +0200 @@ -1064,14 +1064,15 @@ \item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest neighbors. -\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}}) -is a combination of naive Bayes and $k$-nearest neighbors. +\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}} +and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest +neighbors. \end{enum} In addition, the special value \textit{none} is used to disable machine learning by default (cf.\ \textit{smart} below). -The default algorithm is \textit{none}. The algorithm can be selected by +The default algorithm is \textit{nb\_knn}. The algorithm can be selected by setting \texttt{MASH}---either in the environment in which Isabelle is launched, in your \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings} @@ -1083,9 +1084,9 @@ \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the rankings from MePo and MaSh. -\item[\labelitemi] \textbf{\textit{smart}:} -If the learning algorithm is set to be \textit{none} (the default), \textit{smart} -behaves like MePo; otherwise, it combines MePo, MaSh, and MeSh. +\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and +MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart} +behaves like MePo. \end{enum} \opdefault{max\_facts}{smart\_int}{smart} diff -r f55c173a3cbc -r b246943b3aa3 src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options Thu Jul 24 18:46:38 2014 +0200 +++ b/src/HOL/Tools/etc/options Thu Jul 24 18:46:38 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 algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"