further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
authorblanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 427467e227e9de779
parent 42745 b817c6f91a98
child 42747 f132d13fcf75
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4     higher_order_irrel_weight = 1.05,
     1.5     abs_rel_weight = 0.5,
     1.6     abs_irrel_weight = 2.0,
     1.7 -   skolem_irrel_weight = 0.5,
     1.8 +   skolem_irrel_weight = 0.25,
     1.9     theory_const_rel_weight = 0.5,
    1.10     theory_const_irrel_weight = 0.25,
    1.11     chained_const_irrel_weight = 0.25,