--- 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}
--- a/src/HOL/TPTP/mash_eval.ML Mon Dec 10 13:02:56 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Mon Dec 10 13:33:06 2012 +0100
@@ -21,7 +21,7 @@
val MePoN = "MePo"
val MaShN = "MaSh"
-val MeshN = "Mesh"
+val MeShN = "MeSh"
val IsarN = "Isar"
val all_names = map (rpair () o nickname_of) #> Symtab.make
@@ -112,7 +112,7 @@
val [mepo_s, mash_s, mesh_s, isar_s] =
[fn () => prove mepo_ok MePoN fst mepo_facts,
fn () => prove mash_ok MaShN fst mash_facts,
- fn () => prove mesh_ok MeshN I mesh_facts,
+ fn () => prove mesh_ok MeShN I mesh_facts,
fn () => prove isar_ok IsarN fst isar_facts]
|> (* Par_List. *) map (fn f => f ())
in
@@ -138,7 +138,7 @@
["Successes (of " ^ string_of_int n ^ " goals)",
total_of MePoN mepo_ok n,
total_of MaShN mash_ok n,
- total_of MeshN mesh_ok n,
+ total_of MeShN mesh_ok n,
total_of IsarN isar_ok n]
|> cat_lines |> print
end