# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 7e227e9de779b300050899ae36599078d48a307c
# Parent  b817c6f91a98e7c66ad70ed87425f06e1c70ee74
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up

diff -r b817c6f91a98 -r 7e227e9de779 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
@@ -168,7 +168,7 @@
    higher_order_irrel_weight = 1.05,
    abs_rel_weight = 0.5,
    abs_irrel_weight = 2.0,
-   skolem_irrel_weight = 0.5,
+   skolem_irrel_weight = 0.25,
    theory_const_rel_weight = 0.5,
    theory_const_irrel_weight = 0.25,
    chained_const_irrel_weight = 0.25,