--- a/src/Doc/Sledgehammer/document/root.tex Thu Feb 07 11:57:42 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Feb 07 14:05:32 2013 +0100
@@ -1063,10 +1063,11 @@
variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in the
directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
-\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
+\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
+rankings from MePo and MaSh.
-\item[\labelitemi] \textbf{\textit{smart}:} Use MeSh if MaSh is
-enabled and the target prover is an ATP; otherwise, use MePo.
+\item[\labelitemi] \textbf{\textit{smart}:} A mixture of MePo, MaSh, and MeSh if
+MaSh is enabled; otherwise, MePo.
\end{enum}
\opdefault{max\_facts}{smart\_int}{smart}