make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
authorblanchet
Mon, 09 Sep 2013 23:55:35 +0200
changeset 53493 9770b0627de4
parent 53492 c3d7d9911aae
child 53496 cd25f20a797f
make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Sep 09 23:54:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Sep 09 23:55:35 2013 +0200
@@ -387,7 +387,7 @@
 (* High enough so that it isn't wrongly considered as very relevant (e.g., for E
    weights), but low enough so that it is unlikely to be truncated away if few
    facts are included. *)
-val special_fact_index = 75
+val special_fact_index = 45
 
 fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
         (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts