equal
deleted
inserted
replaced
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 |
4 |
5 Sledgehammer's iterative relevance filter (MePo = Meng-Paulson). |
5 Sledgehammer's iterative relevance filter (MePo = Meng-Paulson). |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_FILTER_ITER = |
8 signature SLEDGEHAMMER_MEPO = |
9 sig |
9 sig |
10 type stature = ATP_Problem_Generate.stature |
10 type stature = ATP_Problem_Generate.stature |
11 type fact = Sledgehammer_Fact.fact |
11 type fact = Sledgehammer_Fact.fact |
12 type params = Sledgehammer_Provers.params |
12 type params = Sledgehammer_Provers.params |
13 type relevance_fudge = Sledgehammer_Provers.relevance_fudge |
13 type relevance_fudge = Sledgehammer_Provers.relevance_fudge |
21 val iterative_relevant_facts : |
21 val iterative_relevant_facts : |
22 Proof.context -> params -> string -> int -> relevance_fudge option |
22 Proof.context -> params -> string -> int -> relevance_fudge option |
23 -> term list -> term -> fact list -> fact list |
23 -> term list -> term -> fact list -> fact list |
24 end; |
24 end; |
25 |
25 |
26 structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER = |
26 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = |
27 struct |
27 struct |
28 |
28 |
29 open ATP_Problem_Generate |
29 open ATP_Problem_Generate |
30 open Sledgehammer_Fact |
30 open Sledgehammer_Fact |
31 open Sledgehammer_Provers |
31 open Sledgehammer_Provers |