# HG changeset patch
# User blanchet
# Date 1318880258 -7200
# Node ID 1466037faae4caa472e266664304472a8c5038af
# Parent  170dffc6df751ab258279572eaee3ddea7873e9c
updated doc related to Satallax

diff -r 170dffc6df75 -r 1466037faae4 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Oct 17 21:37:37 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Oct 17 21:37:38 2011 +0200
@@ -523,12 +523,12 @@
 that can be guessed from the number of facts in the original proof and the time
 it took to find it or replay it).
 
-In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
-proofs or sometimes produce incomplete proofs. The minimizer is then invoked to
-find out which facts are actually needed from the (large) set of facts that was
-initinally given to the prover. Finally, if a prover returns a proof with lots
-of facts, the minimizer is invoked automatically since Metis would be unlikely
-to re-find the proof.
+In addition, some provers (e.g., Yices) do not provide proofs or sometimes
+produce incomplete proofs. The minimizer is then invoked to find out which facts
+are actually needed from the (large) set of facts that was initinally given to
+the prover. Finally, if a prover returns a proof with lots of facts, the
+minimizer is invoked automatically since Metis would be unlikely to re-find the
+proof.
 
 \point{A strange error occurred---what should I do?}
 
@@ -737,7 +737,8 @@
 
 \item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
-support for the TPTP many-typed higher-order syntax (THF0).
+support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
+requires version 2.2 or above.
 
 \item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.