# HG changeset patch
# User blanchet
# Date 1404226030 -7200
# Node ID d6df9b63d38530edca5850143fcda7f8fb35c335
# Parent  dabd4516450dbe192c81700732c6a06d382fcc10
updated docs

diff -r dabd4516450d -r d6df9b63d385 src/Doc/Sledgehammer/document/root.tex
--- 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.