# HG changeset patch # User blanchet # Date 1354789510 -3600 # Node ID b7b1f2a170b8da1918cd3adee0cee0a37c9d42ef # Parent ad0ac9112d2c18d754c5f6cc71acede82b34fa39 increase weight of local facts again (MaSh) diff -r ad0ac9112d2c -r b7b1f2a170b8 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 @@ -290,7 +290,7 @@ local -val version = "*** MaSh version 20121205a ***" +val version = "*** MaSh version 20121205b ***" exception Too_New of unit @@ -464,7 +464,7 @@ fun type_feature_of s = ("t" ^ s, 1.0 (* FUDGE *)) fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) fun status_feature_of status = (string_of_status status, 1.0 (* FUDGE *)) -val local_feature = ("local", 1.0 (* FUDGE *)) +val local_feature = ("local", 2.0 (* FUDGE *)) val lams_feature = ("lams", 1.0 (* FUDGE *)) val skos_feature = ("skos", 1.0 (* FUDGE *))