--- a/src/Doc/Sledgehammer/document/root.tex Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Sep 28 11:11:44 2021 +0200
@@ -192,7 +192,7 @@
number (e.g., ``3.6'').
Similarly, if you want to install CVC4, veriT, or Z3, set the environment
-variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{VERIT\_\allowbreak SOLVER},
+variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{ISABELLE\_\allowbreak VERIT},
or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including
the file name}. Ideally, also set \texttt{CVC4\_VERSION},
\texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number
@@ -742,7 +742,7 @@
\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an
SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues.
It is designed to produce detailed proofs for reconstruction in proof
-assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER}
+assistants. To use veriT, set the environment variable \texttt{ISABELLE\_VERIT}
to the complete path of the executable, including the file name.
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at