--- a/src/Doc/Sledgehammer/document/root.tex Sat Jun 28 22:13:23 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Sun Jun 29 18:28:27 2014 +0200
@@ -1059,14 +1059,11 @@
The MaSh machine learner. Three learning engines are provided:
\begin{enum}
-\item[\labelitemi] \textbf{\textit{sml\_nb}} (also called \textbf{\textit{sml}}
+\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{sml\_knn}} is a Standard ML implementation of
+\item[\labelitemi] \textbf{\textit{knn}} is a Standard ML implementation of
$k$-nearest neighbors.
-
-\item[\labelitemi] \textbf{\textit{py}} is a Python implementation of naive Bayes.
-The program is included with Isabelle as \texttt{mash.py}.
\end{enum}
In addition, the special value \textit{none} is used to disable machine learning by
@@ -1077,10 +1074,7 @@
\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}. When switching to the \textit{py} engine,
-you will need to invoke the \textit{relearn\_isar} subcommand
-(\S\ref{sledgehammer}) to synchronize the persistent databases on the
-Python side.
+\texttt{\$ISABELLE\_HOME\_USER/mash}.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.