1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -397,15 +397,16 @@
     1.4  
     1.5  \begin{enum}
     1.6  \item[\labelitemi]
     1.7 -The traditional relevance filter, called \emph{MePo}, assigns a score to every
     1.8 -available fact (lemma, theorem, definition, or axiom) based upon how many
     1.9 -constants that fact shares with the conjecture. This process iterates to include
    1.10 -facts relevant to those just accepted. The constants are weighted to give
    1.11 -unusual ones greater significance. MePo copes best when the conjecture contains
    1.12 -some unusual constants; if all the constants are common, it is unable to
    1.13 -discriminate among the hundreds of facts that are picked up. The filter is also
    1.14 -memoryless: It has no information about how many times a particular fact has
    1.15 -been used in a proof, and it cannot learn.
    1.16 +The traditional relevance filter, called \emph{MePo}
    1.17 +(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact
    1.18 +(lemma, theorem, definition, or axiom) based upon how many constants that fact
    1.19 +shares with the conjecture. This process iterates to include facts relevant to
    1.20 +those just accepted. The constants are weighted to give unusual ones greater
    1.21 +significance. MePo copes best when the conjecture contains some unusual
    1.22 +constants; if all the constants are common, it is unable to discriminate among
    1.23 +the hundreds of facts that are picked up. The filter is also memoryless: It has
    1.24 +no information about how many times a particular fact has been used in a proof,
    1.25 +and it cannot learn.
    1.26  
    1.27  \item[\labelitemi]
    1.28  An experimental, memoryful alternative to MePo is \emph{MaSh}
    1.29 @@ -1019,6 +1020,25 @@
    1.30  \label{relevance-filter}
    1.31  
    1.32  \begin{enum}
    1.33 +\opdefault{fact\_filter}{string}{smart}
    1.34 +Specifies the relevance filter to use. The following filters are available:
    1.35 +
    1.36 +\begin{enum}
    1.37 +\item[\labelitemi] \textbf{\textit{mepo}:}
    1.38 +The traditional memoryless MePo relevance filter.
    1.39 +
    1.40 +\item[\labelitemi] \textbf{\textit{mash}:}
    1.41 +The memoryful MaSh machine learner. MaSh relies on the external program
    1.42 +\texttt{mash}, which can be obtained from the author at \authoremail. To install
    1.43 +it, set the environment variable \texttt{MASH\_HOME} to the directory that
    1.44 +contains the \texttt{mash} executable.
    1.45 +
    1.46 +\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
    1.47 +
    1.48 +\item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if \texttt{mash} is
    1.49 +installed and the target prover is an ATP; otherwise, use MePo.
    1.50 +\end{enum}
    1.51 +
    1.52  \opdefault{max\_facts}{smart\_int}{smart}
    1.53  Specifies the maximum number of facts that may be returned by the relevance
    1.54  filter. If the option is set to \textit{smart}, it is set to a value that was
    1.55 @@ -1033,6 +1053,11 @@
    1.56  iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
    1.57  are relevant and 1 only theorems that refer to previously seen constants.
    1.58  
    1.59 +\optrue{learn}{dont\_learn}
    1.60 +Specifies whether MaSh should be run automatically by Sledgehammer to learn the
    1.61 +available theories (and hence provide more accurate results). Learning only
    1.62 +takes place if \texttt{mash} is installed.
    1.63 +
    1.64  \opdefault{max\_new\_mono\_instances}{int}{smart}
    1.65  Specifies the maximum number of monomorphic instances to generate beyond
    1.66  \textit{max\_facts}. The higher this limit is, the more monomorphic instances

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -323,7 +323,7 @@
     2.4       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
     2.5       learn = learn, fact_filter = fact_filter, max_facts = max_facts,
     2.6       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
     2.7 -     max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
     2.8 +     max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
     2.9       isar_shrink_factor = isar_shrink_factor, slice = slice,
    2.10       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
    2.11       expect = expect}