diff -r a2cbe81e1e32 -r 180ee02eb075 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 28 19:17:31 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jul 29 17:08:46 2021 +0200
@@ -1330,16 +1330,16 @@
 
 \begin{verbatim}
 isabelle mirabelle -d $AFP -O output \
-  -A "sledgehammer[prover=e, prover_timeout=5, keep=/tptp]" \
+  -A "sledgehammer[prover=e, prover_timeout=5, keep=true]" \
   VeriComp
 \end{verbatim}
 
 This command generates TPTP files using Sledgehammer. Since the file
 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}), which must exist beforehand. A TPTP file is generated
-for each subgoal.
+processing the subgoals. The results are written in an action-specific
+subdirectory of the specified output directory (\texttt{output}). A TPTP
+file is generated for each subgoal.
 
 \let\em=\sl
 \bibliography{manual}{}