# HG changeset patch
# User blanchet
# Date 1357322449 -3600
# Node ID 834847691d995a3d1e5fb7a5c4475ca6ec080267
# Parent  58b0b44da54a02df0bd3666fc063310e7cd8947d
updated docs

diff -r 58b0b44da54a -r 834847691d99 NEWS
--- 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
diff -r 58b0b44da54a -r 834847691d99 src/Doc/Sledgehammer/document/root.tex
--- 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