updated docs
authorblanchet
Tue May 20 16:39:13 2014 +0200 (2014-05-20)
changeset 57019f013e3a830c3
parent 57018 142950e9c7e2
child 57020 f7cf92543e6c
updated docs
src/Doc/Sledgehammer/document/root.tex
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue May 20 16:31:39 2014 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Tue May 20 16:39:13 2014 +0200
     1.3 @@ -403,8 +403,7 @@
     1.4  \item[\labelitemi]
     1.5  An experimental alternative to MePo is \emph{MaSh}
     1.6  (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It
     1.7 -relies on an external Python tool that applies machine learning to
     1.8 -the problem of finding relevant facts.
     1.9 +applies machine learning to the problem of finding relevant facts.
    1.10  
    1.11  \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
    1.12  \end{enum}
    1.13 @@ -1068,10 +1067,19 @@
    1.14  The traditional memoryless MePo relevance filter.
    1.15  
    1.16  \item[\labelitemi] \textbf{\textit{mash}:}
    1.17 -The experimental MaSh machine learner. MaSh relies on the external Python
    1.18 -program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set the
    1.19 -environment variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in
    1.20 -the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
    1.21 +The experimental MaSh machine learner.
    1.22 +Two learning engines are provided:
    1.23 +
    1.24 +\begin{enum}
    1.25 +\item[\labelitemi] \emph{sml} (also called \emph{sml\_knn}) refers to a Standard ML implementation
    1.26 +of $k$-nearest neighbors.
    1.27 +
    1.28 +\item[\labelitemi] \emph{py} (also called \emph{yes}) refers to a Python implementation of naive
    1.29 +Bayes. The program is included with Isabelle as \texttt{mash.py}.
    1.30 +\end{enum}
    1.31 +
    1.32 +To enable MaSh, set the environment variable \texttt{MASH} to the name of the desired engine.
    1.33 +Persistent data for both engines is stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
    1.34  
    1.35  \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
    1.36  rankings from MePo and MaSh.