# HG changeset patch
# User blanchet
# Date 1398456797 -7200
# Node ID 1ca7fd5f83bba98ff0fd8d6a25c3a503e4183f6b
# Parent  faa9c21977d29d22b83c3ab1d275706eeb3e49bb
updated Z3 version number

diff -r faa9c21977d2 -r 1ca7fd5f83bb src/Doc/Sledgehammer/document/root.tex
--- 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.