equal
deleted
inserted
replaced
56 val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory |
56 val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory |
57 val smart_store_thms: (bstring * thm list) -> thm list |
57 val smart_store_thms: (bstring * thm list) -> thm list |
58 val smart_store_thms_open: (bstring * thm list) -> thm list |
58 val smart_store_thms_open: (bstring * thm list) -> thm list |
59 val forall_elim_var: int -> thm -> thm |
59 val forall_elim_var: int -> thm -> thm |
60 val forall_elim_vars: int -> thm -> thm |
60 val forall_elim_vars: int -> thm -> thm |
|
61 val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory |
61 val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory |
62 val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory |
62 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory |
63 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory |
63 val note: string -> string * thm -> theory -> thm * theory |
64 val note: string -> string * thm -> theory -> thm * theory |
64 val note_thmss: string -> ((bstring * attribute list) * |
65 val note_thmss: string -> ((bstring * attribute list) * |
65 (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
66 (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
178 |
179 |
179 fun lookup_fact thy xname = |
180 fun lookup_fact thy xname = |
180 let |
181 let |
181 val facts = all_facts_of thy; |
182 val facts = all_facts_of thy; |
182 val name = NameSpace.intern (Facts.space_of facts) xname; |
183 val name = NameSpace.intern (Facts.space_of facts) xname; |
183 in Option.map (pair name) (Facts.lookup facts name) end; |
184 in Option.map (pair name) (Facts.lookup (Context.Theory thy) facts name) end; |
184 |
185 |
185 fun show_result NONE = "none" |
186 fun show_result NONE = "none" |
186 | show_result (SOME (name, _)) = quote name; |
187 | show_result (SOME (name, _)) = quote name; |
187 |
188 |
188 fun get silent theory thmref = |
189 fun get silent theory thmref = |
261 fun name_thms pre official name xs = |
262 fun name_thms pre official name xs = |
262 map (uncurry (name_thm pre official)) (name_multi name xs); |
263 map (uncurry (name_thm pre official)) (name_multi name xs); |
263 |
264 |
264 fun name_thmss official name fact = |
265 fun name_thmss official name fact = |
265 burrow_fact (name_thms true official name) fact; |
266 burrow_fact (name_thms true official name) fact; |
|
267 |
|
268 |
|
269 (* add_thms_dynamic *) |
|
270 |
|
271 fun add_thms_dynamic (bname, f) thy = CRITICAL (fn () => |
|
272 let |
|
273 val name = Sign.full_name thy bname; |
|
274 val r as ref (Thms {theorems, all_facts}) = get_theorems_ref thy; |
|
275 val all_facts' = Facts.add_dynamic (Sign.naming_of thy) (name, f) all_facts; |
|
276 val _ = r := make_thms theorems all_facts'; |
|
277 in thy end); |
266 |
278 |
267 |
279 |
268 (* enter_thms *) |
280 (* enter_thms *) |
269 |
281 |
270 fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); |
282 fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); |
542 |
554 |
543 end; |
555 end; |
544 |
556 |
545 structure BasicPureThy: BASIC_PURE_THY = PureThy; |
557 structure BasicPureThy: BASIC_PURE_THY = PureThy; |
546 open BasicPureThy; |
558 open BasicPureThy; |
|
559 |