tweaked MaSh proximity
authorblanchet
Thu, 06 Dec 2012 11:25:10 +0100
changeset 50398 78c7b52dbadb
parent 50397 d84a5ab736bb
child 50399 52d9720f7a48
tweaked MaSh proximity
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -726,7 +726,7 @@
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =
-  Math.pow (1.3, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+  Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
 
 fun weight_proximity_facts facts =
   facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)