# HG changeset patch
# User desharna
# Date 1623919587 -7200
# Node ID a88427e553711845a61f06fb224974da5c3e928c
# Parent  07675be652278238c47a66134c7bfc7242bb8443
shortened long lines

diff -r 07675be65227 -r a88427e55371 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jun 17 10:43:53 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jun 17 10:46:27 2021 +0200
@@ -1316,7 +1316,9 @@
 \subsection{Example of Benchmarking Multiple Tools}
 
 \begin{verbatim}
-isabelle mirabelle -d $AFP -O output -t 10 -A "try0" -A "metis" VeriComp
+isabelle mirabelle -d $AFP -O output -t 10 \
+  -A "try0" -A "metis" \
+  VeriComp
 \end{verbatim}
 
 This command specifies two actions running the \textbf{try0} and \textbf{metis}
@@ -1327,7 +1329,7 @@
 
 \begin{verbatim}
 isabelle mirabelle -d $AFP -O output \
-  -A "sledgehammer[prover=e, prover_timeout=30], keep=/tptp/files/" \
+  -A "sledgehammer[prover=e, prover_timeout=5, keep=/tptp]" \
   VeriComp
 \end{verbatim}
 
@@ -1335,7 +1337,7 @@
 is generated at the very beginning of every Sledgehammer invocation,
 a timeout of five seconds making the prover fail faster speeds up
 processing the subgoals. The results are written in the specified directory
-(\texttt{/tptp/files/}), which must exist beforehand. A TPTP file is generated
+(\texttt{/tptp}), which must exist beforehand. A TPTP file is generated
 for each subgoal.
 
 \let\em=\sl