--- a/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 13:29:58 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 16:57:19 2014 +0200
@@ -919,12 +919,20 @@
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 versions 4.3.0
+and 4.3.1.
\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
+\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
+executable.
+
\end{sloppy}
-The following remote provers are supported:
+In addition to the local provers, the following remote provers are supported:
\begin{enum}
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of