# HG changeset patch
# User blanchet
# Date 1283175581 -7200
# Node ID c4f0fd1f6e673056a62466e7d7aa6672d059c177
# Parent  c91be1e503bd2b26c98ccbc5012f30f285770763
make Sledgehammer's relevance filter somewhat slacker

diff -r c91be1e503bd -r c4f0fd1f6e67 doc-src/Sledgehammer/sledgehammer.tex
--- 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
diff -r c91be1e503bd -r c4f0fd1f6e67 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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"),