--- a/src/Doc/Sledgehammer/document/root.tex Fri Aug 28 13:37:06 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Aug 28 16:48:05 2015 +0200
@@ -370,7 +370,7 @@
Sledgehammer heuristically selects a few hundred relevant lemmas from the
currently loaded libraries. The component that performs this selection is
-called \emph{relevance filter}.
+called \emph{relevance filter} (\S\ref{relevance-filter}).
\begin{enum}
\item[\labelitemi]
@@ -390,13 +390,10 @@
\underline{S}ledge\underline{h}ammer). It applies machine learning to the
problem of finding relevant facts.
-\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
+\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is
+the default.
\end{enum}
-The default is either MePo or MeSh, depending on whether the environment
-variable \texttt{MASH} is set and what class of provers the target prover
-belongs to (\S\ref{relevance-filter}).
-
The number of facts included in a problem varies from prover to prover, since
some provers get overwhelmed more easily than others. You can show the number of
facts given using the \textit{verbose} option (\S\ref{output-format}) and the
@@ -1018,10 +1015,7 @@
default (cf.\ \textit{smart} below).
The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
-setting \texttt{MASH}---either in the environment in which Isabelle is launched,
-in your
-\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
-file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
+setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
mash}.