--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 20:19:58 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 20:20:10 2010 +0200
@@ -447,7 +447,7 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~90}
+\opdefault{relevance\_thresholds}{int\_pair}{45~85}
Specifies the thresholds above which facts are considered relevant by the
relevance filter. The first threshold is used for the first iteration of the
relevance filter and the second threshold is used for the last iteration (if it