# HG changeset patch # User blanchet # Date 1280353458 -7200 # Node ID 458c4578761fa2c0a2bacfd686fb6cfb806d1274 # Parent a7c9cc973ca1bfe20ae23b039a3fd2acdaf7f9f3 mention version numbers diff -r a7c9cc973ca1 -r 458c4578761f doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 28 23:05:35 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 28 23:44:18 2010 +0200 @@ -147,7 +147,12 @@ Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof}, -\texttt{SPASS}, or \texttt{vampire} executable. +\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested +with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0% +\footnote{Following the rewrite of Vampire, the counter for version numbers was +reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}% +. Since the ATPs' output formats are neither documented nor stable, other +versions of the ATPs might or might not work well with Sledgehammer. \end{enum} To check whether E and SPASS are installed, follow the example in