| changeset 38994 | 7c655a491bce |
| parent 38993 | 504b9e1efd33 |
| child 38996 | 6905ba37376c |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 01 11:36:02 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 01 11:59:04 2010 +0200 @@ -332,7 +332,7 @@ val elim_bonus = Unsynchronized.ref 0.15 val simp_bonus = Unsynchronized.ref 0.15 val local_bonus = Unsynchronized.ref 0.55 -val assum_bonus = Unsynchronized.ref 1.0 +val assum_bonus = Unsynchronized.ref 1.05 val chained_bonus = Unsynchronized.ref 1.5 fun locality_bonus General = 0.0