updated docs
Tue, 20 May 2014 16:39:13 +0200
changeset 57019 f013e3a830c3
parent 57018 142950e9c7e2
child 57020 f7cf92543e6c
updated docs
--- a/src/Doc/Sledgehammer/document/root.tex	Tue May 20 16:31:39 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue May 20 16:39:13 2014 +0200
@@ -403,8 +403,7 @@
 An experimental alternative to MePo is \emph{MaSh}
 (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It
-relies on an external Python tool that applies machine learning to
-the problem of finding relevant facts.
+applies machine learning to the problem of finding relevant facts.
 \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
@@ -1068,10 +1067,19 @@
 The traditional memoryless MePo relevance filter.
 \item[\labelitemi] \textbf{\textit{mash}:}
-The experimental MaSh machine learner. MaSh relies on the external Python
-program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set the
-environment variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in
-the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
+The experimental MaSh machine learner.
+Two learning engines are provided:
+\item[\labelitemi] \emph{sml} (also called \emph{sml\_knn}) refers to a Standard ML implementation
+of $k$-nearest neighbors.
+\item[\labelitemi] \emph{py} (also called \emph{yes}) refers to a Python implementation of naive
+Bayes. The program is included with Isabelle as \texttt{mash.py}.
+To enable MaSh, set the environment variable \texttt{MASH} to the name of the desired engine.
+Persistent data for both engines is stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
 \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
 rankings from MePo and MaSh.