--- a/src/Doc/Sledgehammer/document/root.tex Wed Dec 12 00:14:58 2012 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Dec 12 00:24:06 2012 +0100
@@ -694,9 +694,9 @@
proofs. This happens automatically at Sledgehammer invocations if the
\textit{learn} option (\S\ref{relevance-filter}) is enabled.
-\item[\labelitemi] \textbf{\textit{learn\_atp}:} Invokes MaSh on the current
-theory to process all the available facts, learning from ATP-generated proofs.
-The ATP to use and its timeout can be set using the
+\item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current
+theory to process all the available facts, learning from proofs generated by
+automatic provers. The prover to use and its timeout can be set using the
\textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
(\S\ref{timeouts}) options. It is recommended to perform learning using an
efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
@@ -705,8 +705,8 @@
\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
followed by \textit{learn\_isar}.
-\item[\labelitemi] \textbf{\textit{relearn\_atp}:} Same as \textit{unlearn}
-followed by \textit{learn\_atp}.
+\item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn}
+followed by \textit{learn\_prover}.
\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
currently running machine learners, including elapsed runtime and remaining
@@ -719,8 +719,8 @@
Sledgehammer's behavior can be influenced by various \qty{options}, which can be
specified in brackets after the \textbf{sledgehammer} command. The
\qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
-\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
-example:
+\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional.
+For example:
\prew
\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120]