Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
authorblanchet
Thu, 12 May 2011 15:29:19 +0200
changeset 42746 7e227e9de779
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 file | annotate | diff | comparison | revisions 
--- 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,
isabelle