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 @@ -675,16 +675,35 @@
     1.4  \item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
     1.5  automatic provers.
     1.6  
     1.7 -\item[\labelitemi] \textbf{\textit{unlearn}:} Resets the MaSh machine learner,
     1.8 -erasing any persistent state.
     1.9 +\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
    1.10 +ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
    1.11 +\end{enum}
    1.12  
    1.13 -\item[\labelitemi] \textbf{\textit{learn}:} Invokes the MaSh machine learner on
    1.14 -the current theory to process all the available facts. This happens
    1.15 -automatically at Sledgehammer invocations if the \textit{learn} option
    1.16 -(\S\ref{relevance-filter}) is enabled.
    1.17 +In addition, the following subcommands provide fine control over machine
    1.18 +learning with MaSh:
    1.19  
    1.20 -\item[\labelitemi] \textbf{\textit{relearn}:} Same as \textit{unlearn} followed
    1.21 -by \textit{learn}.
    1.22 +\begin{enum}
    1.23 +\item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any
    1.24 +persistent state.
    1.25 +
    1.26 +\item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current
    1.27 +theory to process all the available facts, learning from their Isabelle/Isar
    1.28 +proofs. This happens automatically at Sledgehammer invocations if the
    1.29 +\textit{learn} option (\S\ref{relevance-filter}) is enabled.
    1.30 +
    1.31 +\item[\labelitemi] \textbf{\textit{learn\_atp}:} Invokes MaSh on the current
    1.32 +theory to process all the available facts, learning from ATP-generated proofs.
    1.33 +The ATP to use and its timeout can be set using the
    1.34 +\textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
    1.35 +(\S\ref{timeouts}) options. It is recommended to perform learning using an
    1.36 +efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
    1.37 +higher-order ATP or an SMT solver.
    1.38 +
    1.39 +\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
    1.40 +followed by \textit{learn\_isar}.
    1.41 +
    1.42 +\item[\labelitemi] \textbf{\textit{relearn\_atp}:} Same as \textit{unlearn}
    1.43 +followed by \textit{learn\_atp}.
    1.44  
    1.45  \item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
    1.46  currently running machine learners, including elapsed runtime and remaining
    1.47 @@ -692,9 +711,6 @@
    1.48  
    1.49  \item[\labelitemi] \textbf{\textit{kill\_learners}:} Terminates all running
    1.50  machine learners.
    1.51 -
    1.52 -\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
    1.53 -ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
    1.54  \end{enum}
    1.55  
    1.56  Sledgehammer's behavior can be influenced by various \qty{options}, which can be
    1.57 @@ -756,9 +772,9 @@
    1.58  All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
    1.59  For convenience, the following aliases are provided:
    1.60  \begin{enum}
    1.61 -\item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.
    1.62 -\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
    1.63 -\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
    1.64 +\item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}.
    1.65 +\item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}.
    1.66 +\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}.
    1.67  \end{enum}
    1.68  
    1.69  \section{Option Reference}