--- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 10:46:27 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 11:27:21 2021 +0200
@@ -1322,7 +1322,7 @@
\end{verbatim}
This command specifies two actions running the \textbf{try0} and \textbf{metis}
-command respectively, both with a timeout of 10 seconds. The results are
+commands, respectively, each with a timeout of 10 seconds. The results are
written to \texttt{output/mirabelle.log}.
\subsection{Example of Generating TPTP Files}