equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML |
|
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Sledgehammer's hybrid relevance filter. |
|
6 *) |
|
7 |
|
8 signature SLEDGEHAMMER_FILTER = |
|
9 sig |
|
10 type stature = ATP_Problem_Generate.stature |
|
11 type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge |
|
12 type relevance_override = Sledgehammer_Filter_Iter.relevance_override |
|
13 |
|
14 val relevant_facts : |
|
15 Proof.context -> real * real -> int |
|
16 -> (string * typ -> term list -> bool * term list) -> relevance_fudge |
|
17 -> relevance_override -> thm list -> term list -> term |
|
18 -> (((unit -> string) * stature) * thm) list |
|
19 -> ((string * stature) * thm) list |
|
20 end; |
|
21 |
|
22 structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = |
|
23 struct |
|
24 |
|
25 open Sledgehammer_Filter_Iter |
|
26 |
|
27 val relevant_facts = iterative_relevant_facts |
|
28 |
|
29 end; |
|