# HG changeset patch
# User desharna
# Date 1632820304 -7200
# Node ID d5e034f2c109f4479b98dda18005456b166f80f2
# Parent  d8dc8fdc46fc913da9fbd257ca21c4bb189431db
fixed veriT environment variable in sledgehammer's documentation

diff -r d8dc8fdc46fc -r d5e034f2c109 src/Doc/Sledgehammer/document/root.tex
--- 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