doc-src/Sledgehammer/sledgehammer.tex
changeset 37414 d0cea0796295
parent 36926 90bb12cf8e36
child 37498 b426cbdb5a23
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 14 16:17:20 2010 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 14 16:43:44 2010 +0200
     1.3 @@ -338,11 +338,13 @@
     1.4  Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
     1.5  environment variable \texttt{SPASS\_HOME} to the directory that contains the
     1.6  \texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
     1.7 -download page. See \S\ref{installation} for details.
     1.8 +download page. Sledgehammer requires version 3.5 or above. See
     1.9 +\S\ref{installation} for details.
    1.10  
    1.11 -\item[$\bullet$] \textbf{\textit{spass\_tptp}:} Same as the above, except that
    1.12 -Sledgehammer communicates with SPASS using the TPTP syntax rather than the
    1.13 -native DFG syntax. This ATP is provided for experimental purposes.
    1.14 +\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that
    1.15 +Sledgehammer communicates with SPASS using the native DFG syntax rather than the
    1.16 +TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided
    1.17 +for compatibility reasons.
    1.18  
    1.19  \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
    1.20  Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use