--- a/src/Doc/Sledgehammer/document/root.tex Tue May 20 21:13:21 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue May 20 22:28:08 2014 +0200
@@ -166,10 +166,10 @@
\footnote{Vampire's and Yices's licenses prevent us from doing the same for
these otherwise remarkable tools.}
For Z3, you must additionally set the variable
-\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
+\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
noncommercial user---either in the environment in which Isabelle is
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
-via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
+via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
@@ -907,10 +907,10 @@
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
+name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
noncommercial user---either in the environment in which Isabelle is
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
-via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
+via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
versions 3.0, 3.1, 3.2, and 4.0.
@@ -918,7 +918,7 @@
are treated as a different prover by Isabelle. To use these, set the environment
variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
-``yes'', as described above. Sledgehammer has been tested with a pre-release
+\textit{yes}, as described above. Sledgehammer has been tested with a pre-release
version of 4.3.2.
\end{enum}
@@ -1067,19 +1067,27 @@
The traditional memoryless MePo relevance filter.
\item[\labelitemi] \textbf{\textit{mash}:}
-The experimental MaSh machine learner.
-Two learning engines are provided:
+The experimental MaSh machine learner. Three learning engines are provided:
\begin{enum}
-\item[\labelitemi] \emph{sml} (also called \emph{sml\_knn}) refers to a Standard ML implementation
-of $k$-nearest neighbors.
+\item[\labelitemi] \textbf{\textit{sml}} (also called
+\textbf{\textit{sml\_knn}}) is 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}.
+\item[\labelitemi] \textbf{\textit{sml\_nb}} is a Standard ML implementation of
+naive Bayes.
+
+\item[\labelitemi] \textbf{\textit{py}} (also called \textbf{\textit{yes}}) is a
+Python implementation of naive Bayes. The program is included with Isabelle as
+\texttt{mash.py}.
\end{enum}
-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}.
+To enable MaSh, set the variable \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}.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.