equal
deleted
inserted
replaced
214 (* axioms and defs *) |
214 (* axioms and defs *) |
215 |
215 |
216 fun add_axms f args thy = |
216 fun add_axms f args thy = |
217 f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; |
217 f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; |
218 |
218 |
219 val add_axioms = add_axms PureThy.add_axioms o map Comment.ignore; |
219 val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore; |
220 val add_axioms_i = PureThy.add_axioms_i o map Comment.ignore; |
220 val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore; |
221 val add_defs = add_axms PureThy.add_defs o map Comment.ignore; |
221 val add_defs = add_axms (#1 oo PureThy.add_defs) o map Comment.ignore; |
222 val add_defs_i = PureThy.add_defs_i o map Comment.ignore; |
222 val add_defs_i = (#1 oo PureThy.add_defs_i) o map Comment.ignore; |
223 |
223 |
224 |
224 |
225 (* constdefs *) |
225 (* constdefs *) |
226 |
226 |
227 fun gen_add_constdefs consts defs args thy = |
227 fun gen_add_constdefs consts defs args thy = |