author blanchet Fri, 25 Apr 2014 22:13:17 +0200 changeset 56725 1ca7fd5f83bb parent 56724 faa9c21977d2 child 56726 9fba10c97aef
updated Z3 version number
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Apr 25 22:13:17 2014 +0200
@@ -919,14 +919,14 @@
are treated as a different prover by Isabelle. To use these, set the environment
variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
-yes'', as described above. Sledgehammer has been tested with versions 4.3.0
-and 4.3.1.
+yes'', as described above. Sledgehammer has been tested with a pre-release
+version of 4.3.2.
\end{enum}

\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
formats (FOF and TFF0). It is included for experimental purposes. It requires
-version 4.3.1 of Z3 above. To use it, set the environment variable
+version 4.3.1 of Z3 or above. To use it, set the environment variable
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
executable.