equal
deleted
inserted
replaced
20 struct |
20 struct |
21 |
21 |
22 open ATP_Systems |
22 open ATP_Systems |
23 open ATP_Translate |
23 open ATP_Translate |
24 open Sledgehammer_Util |
24 open Sledgehammer_Util |
|
25 open Sledgehammer_Filter |
25 open Sledgehammer_Provers |
26 open Sledgehammer_Provers |
26 open Sledgehammer_Minimize |
27 open Sledgehammer_Minimize |
27 open Sledgehammer_Run |
28 open Sledgehammer_Run |
28 |
29 |
29 val sledgehammerN = "sledgehammer" |
30 val sledgehammerN = "sledgehammer" |
44 (Preferences.bool_pref auto "auto-sledgehammer" |
45 (Preferences.bool_pref auto "auto-sledgehammer" |
45 "Run Sledgehammer automatically.") |
46 "Run Sledgehammer automatically.") |
46 |
47 |
47 (** Sledgehammer commands **) |
48 (** Sledgehammer commands **) |
48 |
49 |
49 val no_relevance_override = {add = [], del = [], only = false} |
|
50 fun add_relevance_override ns : relevance_override = |
50 fun add_relevance_override ns : relevance_override = |
51 {add = ns, del = [], only = false} |
51 {add = ns, del = [], only = false} |
52 fun del_relevance_override ns : relevance_override = |
52 fun del_relevance_override ns : relevance_override = |
53 {add = [], del = ns, only = false} |
53 {add = [], del = ns, only = false} |
54 fun only_relevance_override ns : relevance_override = |
54 fun only_relevance_override ns : relevance_override = |