add one option to Mirabelle
authorblanchet
Tue, 31 Aug 2010 20:23:32 +0200
changeset 38941 e2c95e3263a4
parent 38940 cad88d38e3c6
child 38942 e10c11971fa7
add one option to Mirabelle
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 20:20:10 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 20:23:32 2010 +0200
@@ -7,6 +7,8 @@
 
 val relevance_filter_args =
   [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
+   ("higher_order_irrel_weight",
+    Sledgehammer_Fact_Filter.higher_order_irrel_weight),
    ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
    ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
    ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),