1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 16 10:22:06 2014 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 16 17:57:27 2014 +0200
     1.3 @@ -1064,15 +1064,14 @@
     1.4  \item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest
     1.5  neighbors.
     1.6  
     1.7 -\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}}
     1.8 -and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest
     1.9 -neighbors.
    1.10 +\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}})
    1.11 +is a combination of naive Bayes and $k$-nearest neighbors.
    1.12  \end{enum}
    1.13  
    1.14  In addition, the special value \textit{none} is used to disable machine learning by
    1.15  default (cf.\ \textit{smart} below).
    1.16  
    1.17 -The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
    1.18 +The default algorithm is \textit{none}. The algorithm can be selected by
    1.19  setting \texttt{MASH}---either in the environment in which Isabelle is launched,
    1.20  in your
    1.21  \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
    1.22 @@ -1084,9 +1083,9 @@
    1.23  \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
    1.24  rankings from MePo and MaSh.
    1.25  
    1.26 -\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
    1.27 -MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart}
    1.28 -behaves like MePo.
    1.29 +\item[\labelitemi] \textbf{\textit{smart}:}
    1.30 +If the learning algorithm is set to be \textit{none} (the default), \textit{smart}
    1.31 +behaves like MePo; otherwise, it combines MePo, MaSh, and MeSh.
    1.32  \end{enum}
    1.33  
    1.34  \opdefault{max\_facts}{smart\_int}{smart}

     2.1 --- a/src/HOL/Tools/etc/options	Wed Jul 16 10:22:06 2014 +0200
     2.2 +++ b/src/HOL/Tools/etc/options	Wed Jul 16 17:57:27 2014 +0200
     2.3 @@ -35,5 +35,5 @@
     2.4  public option z3_non_commercial : string = "unknown"
     2.5    -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     2.6  
     2.7 -public option MaSh : string = "sml"
     2.8 +public option MaSh : string = "none"
     2.9    -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"