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