src/Doc/Sledgehammer/document/root.tex
changeset 57028 e5466055e94f
parent 57019 f013e3a830c3
child 57029 75cc30d2b83f
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue May 20 21:13:21 2014 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Tue May 20 22:28:08 2014 +0200
     1.3 @@ -166,10 +166,10 @@
     1.4  \footnote{Vampire's and Yices's licenses prevent us from doing the same for
     1.5  these otherwise remarkable tools.}
     1.6  For Z3, you must additionally set the variable
     1.7 -\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
     1.8 +\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
     1.9  noncommercial user---either in the environment in which Isabelle is
    1.10  launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
    1.11 -via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
    1.12 +via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
    1.13  > Isabelle > General'' in Isabelle/jEdit.
    1.14  
    1.15  \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
    1.16 @@ -907,10 +907,10 @@
    1.17  \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
    1.18  Microsoft Research \cite{z3}. To use Z3, set the environment variable
    1.19  \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
    1.20 -name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
    1.21 +name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
    1.22  noncommercial user---either in the environment in which Isabelle is
    1.23  launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
    1.24 -via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
    1.25 +via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
    1.26  > Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
    1.27  versions 3.0, 3.1, 3.2, and 4.0.
    1.28  
    1.29 @@ -918,7 +918,7 @@
    1.30  are treated as a different prover by Isabelle. To use these, set the environment
    1.31  variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
    1.32  including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
    1.33 -``yes'', as described above. Sledgehammer has been tested with a pre-release
    1.34 +\textit{yes}, as described above. Sledgehammer has been tested with a pre-release
    1.35  version of 4.3.2.
    1.36  \end{enum}
    1.37  
    1.38 @@ -1067,19 +1067,27 @@
    1.39  The traditional memoryless MePo relevance filter.
    1.40  
    1.41  \item[\labelitemi] \textbf{\textit{mash}:}
    1.42 -The experimental MaSh machine learner.
    1.43 -Two learning engines are provided:
    1.44 +The experimental MaSh machine learner. Three learning engines are provided:
    1.45  
    1.46  \begin{enum}
    1.47 -\item[\labelitemi] \emph{sml} (also called \emph{sml\_knn}) refers to a Standard ML implementation
    1.48 -of $k$-nearest neighbors.
    1.49 +\item[\labelitemi] \textbf{\textit{sml}} (also called
    1.50 +\textbf{\textit{sml\_knn}}) is a Standard ML implementation of $k$-nearest
    1.51 +neighbors.
    1.52  
    1.53 -\item[\labelitemi] \emph{py} (also called \emph{yes}) refers to a Python implementation of naive
    1.54 -Bayes. The program is included with Isabelle as \texttt{mash.py}.
    1.55 +\item[\labelitemi] \textbf{\textit{sml\_nb}} is a Standard ML implementation of
    1.56 +naive Bayes.
    1.57 +
    1.58 +\item[\labelitemi] \textbf{\textit{py}} (also called \textbf{\textit{yes}}) is a
    1.59 +Python implementation of naive Bayes. The program is included with Isabelle as
    1.60 +\texttt{mash.py}.
    1.61  \end{enum}
    1.62  
    1.63 -To enable MaSh, set the environment variable \texttt{MASH} to the name of the desired engine.
    1.64 -Persistent data for both engines is stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
    1.65 +To enable MaSh, set the variable \texttt{MASH} to the name of the desired
    1.66 +engine---either in the environment in which Isabelle is launched, in your
    1.67 +\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``Mash'' option
    1.68 +under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
    1.69 +Persistent data for both engines is stored in the directory
    1.70 +\texttt{\$ISABELLE\_HOME\_USER/mash}.
    1.71  
    1.72  \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
    1.73  rankings from MePo and MaSh.