src/Doc/Sledgehammer/document/root.tex

 \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
 automatic provers supported by Sledgehammer. See \S\ref{installation} and
 \S\ref{mode-of-operation} for more information on how to install automatic
 provers.
 
-\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about
-currently running automatic provers, including elapsed runtime and remaining
-time until timeout.
-
-\item[\labelitemi] \textbf{\textit{kill\_all}:} Terminates all running
-threads (automatic provers and machine learners).
-
 \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
 ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
 \end{enum}
 
 In addition, the following subcommands provide finer control over machine

 \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
 followed by \textit{learn\_isar}.
 
 \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,