equal
deleted
inserted
replaced
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 signature SLEDGEHAMMER_FACT_FILTER = |
6 signature SLEDGEHAMMER_FACT_FILTER = |
7 sig |
7 sig |
8 type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm |
8 type cnf_thm = Clausifier.cnf_thm |
9 |
9 |
10 type relevance_override = |
10 type relevance_override = |
11 {add: Facts.ref list, |
11 {add: Facts.ref list, |
12 del: Facts.ref list, |
12 del: Facts.ref list, |
13 only: bool} |
13 only: bool} |
19 end; |
19 end; |
20 |
20 |
21 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = |
21 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = |
22 struct |
22 struct |
23 |
23 |
|
24 open Clausifier |
24 open Sledgehammer_FOL_Clause |
25 open Sledgehammer_FOL_Clause |
25 open Sledgehammer_Fact_Preprocessor |
|
26 open Sledgehammer_HOL_Clause |
26 open Sledgehammer_HOL_Clause |
27 |
27 |
28 (* Experimental feature: Filter theorems in natural form or in CNF? *) |
28 (* Experimental feature: Filter theorems in natural form or in CNF? *) |
29 val use_natural_form = Unsynchronized.ref false |
29 val use_natural_form = Unsynchronized.ref false |
30 |
30 |