summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | desharna |

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

--- 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