# HG changeset patch
# User blanchet
# Date 1355142786 -3600
# Node ID 52ec07a7f30489499920e545f94a8c8c6fd11340
# Parent  85739c08d1263da280164eec839c2eedb4480bdc
changed capitalization of MeSh filter

diff -r 85739c08d126 -r 52ec07a7f304 src/Doc/Sledgehammer/document/root.tex
--- 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}
 
diff -r 85739c08d126 -r 52ec07a7f304 src/HOL/TPTP/mash_eval.ML
--- 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