author | blanchet |
Thu, 06 Dec 2012 11:25:10 +0100 | |
changeset 50398 | 78c7b52dbadb |
parent 50397 | d84a5ab736bb |
child 50399 | 52d9720f7a48 |
--- 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)