equal
deleted
inserted
replaced
8 signature SLEDGEHAMMER_FILTER = |
8 signature SLEDGEHAMMER_FILTER = |
9 sig |
9 sig |
10 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained |
10 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained |
11 |
11 |
12 type relevance_fudge = |
12 type relevance_fudge = |
13 {allow_ext : bool, |
13 {local_const_multiplier : real, |
14 local_const_multiplier : real, |
|
15 worse_irrel_freq : real, |
14 worse_irrel_freq : real, |
16 higher_order_irrel_weight : real, |
15 higher_order_irrel_weight : real, |
17 abs_rel_weight : real, |
16 abs_rel_weight : real, |
18 abs_irrel_weight : real, |
17 abs_irrel_weight : real, |
19 skolem_irrel_weight : real, |
18 skolem_irrel_weight : real, |
81 | is_locality_global Assum = false |
80 | is_locality_global Assum = false |
82 | is_locality_global Chained = false |
81 | is_locality_global Chained = false |
83 | is_locality_global _ = true |
82 | is_locality_global _ = true |
84 |
83 |
85 type relevance_fudge = |
84 type relevance_fudge = |
86 {allow_ext : bool, |
85 {local_const_multiplier : real, |
87 local_const_multiplier : real, |
|
88 worse_irrel_freq : real, |
86 worse_irrel_freq : real, |
89 higher_order_irrel_weight : real, |
87 higher_order_irrel_weight : real, |
90 abs_rel_weight : real, |
88 abs_rel_weight : real, |
91 abs_irrel_weight : real, |
89 abs_irrel_weight : real, |
92 skolem_irrel_weight : real, |
90 skolem_irrel_weight : real, |