src/Doc/Sledgehammer/document/root.tex

 \item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current
 theory to process all the available facts, learning from their Isabelle/Isar
 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
 higher-order ATP or an SMT solver.
 
 \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
 time until timeout.
 

 \end{enum}
 
 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]
 \postw