fixed veriT environment variable in sledgehammer's documentation draft
authordesharna
Tue, 28 Sep 2021 11:11:44 +0200
changeset 74739 d7cc3b919566
parent 74738 d8dc8fdc46fc
child 74740 bc712fb8ccaa
fixed veriT environment variable in sledgehammer's documentation
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