--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:05:22 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:32:43 2010 +0200
@@ -469,10 +469,10 @@
it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
because empirical results suggest that these are the best settings.
-\opfalse{defs\_relevant}{defs\_irrelevant}
-Specifies whether the definition of constants occurring in the formula to prove
-should be considered particularly relevant. Enabling this option tends to lead
-to larger problems and typically slows down the ATPs.
+%\opfalse{defs\_relevant}{defs\_irrelevant}
+%Specifies whether the definition of constants occurring in the formula to prove
+%should be considered particularly relevant. Enabling this option tends to lead
+%to larger problems and typically slows down the ATPs.
\end{enum}