--- a/src/Doc/Sledgehammer/document/root.tex Mon Dec 10 13:02:56 2012 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Dec 10 13:33:06 2012 +0100
@@ -417,10 +417,10 @@
relies on an external Python tool that 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.
\end{enum}
-The default is either MePo or Mesh, depending on whether the environment
+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}).
@@ -1062,7 +1062,7 @@
\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
-\item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if MaSh is
+\item[\labelitemi] \textbf{\textit{smart}:} Use MeSh if MaSh is
enabled and the target prover is an ATP; otherwise, use MePo.
\end{enum}