# 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