equal
deleted
inserted
replaced
36 only : bool} |
36 only : bool} |
37 |
37 |
38 val trace : bool Config.T |
38 val trace : bool Config.T |
39 val ignore_no_atp : bool Config.T |
39 val ignore_no_atp : bool Config.T |
40 val instantiate_inducts : bool Config.T |
40 val instantiate_inducts : bool Config.T |
|
41 val no_relevance_override : relevance_override |
41 val const_names_in_fact : |
42 val const_names_in_fact : |
42 theory -> (string * typ -> term list -> bool * term list) -> term |
43 theory -> (string * typ -> term list -> bool * term list) -> term |
43 -> string list |
44 -> string list |
44 val fact_from_ref : |
45 val fact_from_ref : |
45 Proof.context -> unit Symtab.table -> thm list |
46 Proof.context -> unit Symtab.table -> thm list |
97 |
98 |
98 type relevance_override = |
99 type relevance_override = |
99 {add : (Facts.ref * Attrib.src list) list, |
100 {add : (Facts.ref * Attrib.src list) list, |
100 del : (Facts.ref * Attrib.src list) list, |
101 del : (Facts.ref * Attrib.src list) list, |
101 only : bool} |
102 only : bool} |
|
103 |
|
104 val no_relevance_override = {add = [], del = [], only = false} |
102 |
105 |
103 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
106 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
104 val abs_name = sledgehammer_prefix ^ "abs" |
107 val abs_name = sledgehammer_prefix ^ "abs" |
105 val skolem_prefix = sledgehammer_prefix ^ "sko" |
108 val skolem_prefix = sledgehammer_prefix ^ "sko" |
106 val theory_const_suffix = Long_Name.separator ^ " 1" |
109 val theory_const_suffix = Long_Name.separator ^ " 1" |