12 |
12 |
13 type raw_fact = ((unit -> string) * stature) * thm |
13 type raw_fact = ((unit -> string) * stature) * thm |
14 type fact = (string * stature) * thm |
14 type fact = (string * stature) * thm |
15 |
15 |
16 type fact_override = |
16 type fact_override = |
17 {add : (Facts.ref * Attrib.src list) list, |
17 {add : (Facts.ref * Token.src list) list, |
18 del : (Facts.ref * Attrib.src list) list, |
18 del : (Facts.ref * Token.src list) list, |
19 only : bool} |
19 only : bool} |
20 |
20 |
21 val instantiate_inducts : bool Config.T |
21 val instantiate_inducts : bool Config.T |
22 val no_fact_override : fact_override |
22 val no_fact_override : fact_override |
23 |
23 |
24 val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> |
24 val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> |
25 Facts.ref * Attrib.src list -> ((string * stature) * thm) list |
25 Facts.ref * Token.src list -> ((string * stature) * thm) list |
26 val backquote_thm : Proof.context -> thm -> string |
26 val backquote_thm : Proof.context -> thm -> string |
27 val is_blacklisted_or_something : Proof.context -> bool -> string -> bool |
27 val is_blacklisted_or_something : Proof.context -> bool -> string -> bool |
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
29 val build_name_tables : (thm -> string) -> ('a * thm) list -> |
29 val build_name_tables : (thm -> string) -> ('a * thm) list -> |
30 string Symtab.table * string Symtab.table |
30 string Symtab.table * string Symtab.table |
48 |
48 |
49 type raw_fact = ((unit -> string) * stature) * thm |
49 type raw_fact = ((unit -> string) * stature) * thm |
50 type fact = (string * stature) * thm |
50 type fact = (string * stature) * thm |
51 |
51 |
52 type fact_override = |
52 type fact_override = |
53 {add : (Facts.ref * Attrib.src list) list, |
53 {add : (Facts.ref * Token.src list) list, |
54 del : (Facts.ref * Attrib.src list) list, |
54 del : (Facts.ref * Token.src list) list, |
55 only : bool} |
55 only : bool} |
56 |
56 |
57 (* gracefully handle huge background theories *) |
57 (* gracefully handle huge background theories *) |
58 val max_facts_for_duplicates = 50000 |
58 val max_facts_for_duplicates = 50000 |
59 val max_facts_for_complex_check = 25000 |
59 val max_facts_for_complex_check = 25000 |
157 (scope_of_thm global assms chained th, status_of_thm css name th) |
157 (scope_of_thm global assms chained th, status_of_thm css name th) |
158 |
158 |
159 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) = |
159 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) = |
160 let |
160 let |
161 val ths = Attrib.eval_thms ctxt [xthm] |
161 val ths = Attrib.eval_thms ctxt [xthm] |
162 val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args) |
162 val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args) |
163 |
163 |
164 fun nth_name j = |
164 fun nth_name j = |
165 (case xref of |
165 (case xref of |
166 Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket |
166 Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket |
167 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
167 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |