--- a/NEWS Fri Jan 04 19:00:49 2013 +0100
+++ b/NEWS Fri Jan 04 19:00:49 2013 +0100
@@ -139,7 +139,7 @@
Sledgehammer manual for details.
- Polished Isar proofs generated with "isar_proofs" option.
- Rationalized type encodings ("type_enc" option).
- - Renamed "kill_provers" subcommand to "kill".
+ - Renamed "kill_provers" subcommand to "kill_all".
- Renamed options:
isar_proof ~> isar_proofs
isar_shrink_factor ~> isar_shrink
--- a/src/Doc/Sledgehammer/document/root.tex Fri Jan 04 19:00:49 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Jan 04 19:00:49 2013 +0100
@@ -675,7 +675,7 @@
currently running automatic provers, including elapsed runtime and remaining
time until timeout.
-\item[\labelitemi] \textbf{\textit{kill}:} Terminates all running
+\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
@@ -711,9 +711,6 @@
\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
currently running machine learners, including elapsed runtime and remaining
time until timeout.
-
-\item[\labelitemi] \textbf{\textit{kill\_learners}:} Terminates all running
-machine learners.
\end{enum}
Sledgehammer's behavior can be influenced by various \qty{options}, which can be