--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 30 15:39:27 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 30 15:39:41 2010 +0200
@@ -447,7 +447,7 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~95}
+\opdefault{relevance\_thresholds}{int\_pair}{45~90}
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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 30 15:39:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 30 15:39:41 2010 +0200
@@ -67,7 +67,7 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_thresholds", "45 95"),
+ ("relevance_thresholds", "45 90"),
("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),