# HG changeset patch
# User blanchet
# Date 1381264385 -7200
# Node ID fcb7bbbe379992ea7bf5817093b50d2f924446a2
# Parent  c7e9f1df30bb7f50264e57675447f73c1e8447be
higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"

diff -r c7e9f1df30bb -r fcb7bbbe3799 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Oct 08 21:19:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Oct 08 22:33:05 2013 +0200
@@ -311,7 +311,7 @@
    max_imperfect = 11.5,
    max_imperfect_exp = 1.0,
    threshold_divisor = 2.0,
-   ridiculous_threshold = 0.01}
+   ridiculous_threshold = 0.1}
 
 (* FUDGE (FIXME) *)
 val smt_relevance_fudge =