--- 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
@@ -172,6 +172,7 @@
skolem_irrel_weight = 0.75,
theory_const_rel_weight = 0.5,
theory_const_irrel_weight = 0.25,
+ chained_const_irrel_weight = 0.25,
intro_bonus = 0.15,
elim_bonus = 0.15,
simp_bonus = 0.15,
@@ -194,6 +195,7 @@
skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
+ chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge,
intro_bonus = #intro_bonus atp_relevance_fudge,
elim_bonus = #elim_bonus atp_relevance_fudge,
simp_bonus = #simp_bonus atp_relevance_fudge,