# 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,