equal
deleted
inserted
replaced
172 (base_sort, judgment, (atomize, Thm.add_thm th rulify))); |
172 (base_sort, judgment, (atomize, Thm.add_thm th rulify))); |
173 |
173 |
174 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I); |
174 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I); |
175 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I); |
175 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I); |
176 |
176 |
177 val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs)); |
177 val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs); |
178 |
178 |
179 |
179 |
180 (* atomize *) |
180 (* atomize *) |
181 |
181 |
182 fun atomize_term thy = |
182 fun atomize_term thy = |