equal
deleted
inserted
replaced
305 (* apply theorems and attributes *) |
305 (* apply theorems and attributes *) |
306 |
306 |
307 local |
307 local |
308 |
308 |
309 val app_facts = |
309 val app_facts = |
310 apfst flat oo fold_map (fn (thms, atts) => fn thy => |
310 fold_maps (fn (thms, atts) => fn thy => |
311 fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy); |
311 fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy); |
312 |
312 |
313 in |
313 in |
314 |
314 |
315 fun apply_facts name_flags1 name_flags2 (b, facts) thy = |
315 fun apply_facts name_flags1 name_flags2 (b, facts) thy = |