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.
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
authorblanchet
Wed, 16 May 2012 18:16:51 +0200
changeset 47934 08d7aff8c7e6
parent 47933 4e8e0245e8be
child 47935 631ea563c20a
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 16 18:16:51 2012 +0200
@@ -223,7 +223,7 @@
    higher_order_irrel_weight = 1.05,
    abs_rel_weight = 0.5,
    abs_irrel_weight = 2.0,
-   skolem_irrel_weight = 0.25,
+   skolem_irrel_weight = 0.05,
    theory_const_rel_weight = 0.5,
    theory_const_irrel_weight = 0.25,
    chained_const_irrel_weight = 0.25,
isabelle