# HG changeset patch # User blanchet # Date 1377500852 -7200 # Node ID 6c5e7143e1f65695a807a687a57a345e24969091 # Parent 942a1b48bb310ce4637d9b920e4099fe350ba4be tuned fudge factor in light of evaluation diff -r 942a1b48bb31 -r 6c5e7143e1f6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 25 23:20:25 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Aug 26 09:07:32 2013 +0200 @@ -902,9 +902,9 @@ fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm -val chained_feature_factor = 0.5 -val extra_feature_factor = 0.1 -val num_extra_feature_facts = 10 (* FUDGE *) +val chained_feature_factor = 0.5 (* FUDGE *) +val extra_feature_factor = 0.1 (* FUDGE *) +val num_extra_feature_facts = 5 (* FUDGE *) (* FUDGE *) fun weight_of_proximity_fact rank =