equal
deleted
inserted
replaced
169 |
169 |
170 (** treatment of meta-level connectives **) |
170 (** treatment of meta-level connectives **) |
171 |
171 |
172 (* maintain rules *) |
172 (* maintain rules *) |
173 |
173 |
174 val get_atomize = #1 o #atomize_rulify o get_data; |
174 fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt))); |
175 val get_rulify = #2 o #atomize_rulify o get_data; |
175 val get_atomize = get_atomize_rulify #1; |
|
176 val get_rulify = get_atomize_rulify #2; |
176 |
177 |
177 fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) => |
178 fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) => |
178 (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify))); |
179 (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify))); |
179 |
180 |
180 fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) => |
181 fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) => |