# HG changeset patch
# User blanchet
# Date 1314105526 -7200
# Node ID a39d94de1aeb7392407b7a9dcf334256a9bb642a
# Parent  3d0921b91a8643d57935ee2d6618a6dd6be343c8
updated Z3 docs

diff -r 3d0921b91a86 -r a39d94de1aeb doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 23 15:15:43 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 23 15:18:46 2011 +0200
@@ -762,12 +762,13 @@
 \item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable
 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name, and set \texttt{Z3\_NON\_COMMERCIAL=yes} to confirm that you are a
+name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
 noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
 
 \item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
-ATP, exploiting Z3's undocumented support for the TPTP format. It is included
-for experimental purposes. It requires version 2.18 or above.
+ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
+formats (FOF and TFF). It is included for experimental purposes. It requires
+version 3.0 or above.
 \end{enum}
 
 In addition, the following remote provers are supported: