equal
deleted
inserted
replaced
161 |
161 |
162 |
162 |
163 (* axioms *) |
163 (* axioms *) |
164 |
164 |
165 fun add_axms f args thy = |
165 fun add_axms f args thy = |
166 f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy; |
166 f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy; |
167 |
167 |
168 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd); |
168 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd); |
169 |
169 |
170 fun add_defs ((unchecked, overloaded), args) = |
170 fun add_defs ((unchecked, overloaded), args) = |
171 add_axms |
171 add_axms |