--- 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}
--- 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)"