--- a/src/Doc/Sledgehammer/document/root.tex Thu Aug 20 11:52:45 2020 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Aug 20 11:52:46 2020 +0200
@@ -836,10 +836,12 @@
to the directory that contains the \texttt{z3\_tptp} executable.
\item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition
-\cite{cruanes-2014} is a first-order resolution prover developed by Simon
+\cite{cruanes-2014} is a higher-order superposition prover developed by Simon
Cruanes and colleagues. To use Zipperposition, set the environment variable
\texttt{ZIPPERPOSITION\_HOME} to the directory that contains the
-\texttt{zipperposition} executable.
+\texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the
+version number (e.g., ``2.0.1''). Sledgehammer has been tested with version
+2.0.1.
\end{enum}
\end{sloppy}