--- a/src/Doc/Sledgehammer/document/root.tex Tue Jul 01 16:47:10 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Jul 01 16:47:10 2014 +0200
@@ -1059,22 +1059,26 @@
The MaSh machine learner. Three learning engines are provided:
\begin{enum}
-\item[\labelitemi] \textbf{\textit{nb}} (also called \textbf{\textit{sml}}
-and \textbf{\textit{yes}}) is a Standard ML implementation of naive Bayes.
+\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
-\item[\labelitemi] \textbf{\textit{knn}} is a Standard ML implementation of
-$k$-nearest neighbors.
+\item[\labelitemi] \textbf{\textit{knn}} is an implementation of $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 engine can be selected by setting \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
-under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
-Persistent data for both engines is stored in the directory
-\texttt{\$ISABELLE\_HOME\_USER/mash}.
+The default engine is \textit{nb\_knn}. The engine can be selected by setting
+\texttt{MASH} to the name of the desired engine---either in the environment in
+which Isabelle is launched, in your
+\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak 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\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.