src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 53197 6c5e7143e1f6
parent 53159 a5805fe4e91c
child 53201 2a2dc18f3e10
equal deleted inserted replaced
53196:942a1b48bb31 53197:6c5e7143e1f6
   900   map (nickname_of_thm o snd)
   900   map (nickname_of_thm o snd)
   901   #> maximal_wrt_graph access_G
   901   #> maximal_wrt_graph access_G
   902 
   902 
   903 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
   903 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
   904 
   904 
   905 val chained_feature_factor = 0.5
   905 val chained_feature_factor = 0.5 (* FUDGE *)
   906 val extra_feature_factor = 0.1
   906 val extra_feature_factor = 0.1 (* FUDGE *)
   907 val num_extra_feature_facts = 10 (* FUDGE *)
   907 val num_extra_feature_facts = 5 (* FUDGE *)
   908 
   908 
   909 (* FUDGE *)
   909 (* FUDGE *)
   910 fun weight_of_proximity_fact rank =
   910 fun weight_of_proximity_fact rank =
   911   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
   911   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
   912 
   912