equal
deleted
inserted
replaced
191 (base_sort, judgment, (atomize, Thm.add_thm th rulify))); |
191 (base_sort, judgment, (atomize, Thm.add_thm th rulify))); |
192 |
192 |
193 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I); |
193 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I); |
194 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I); |
194 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I); |
195 |
195 |
196 val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq); |
196 val _ = Context.>> (add_rulify Drule.norm_hhf_eq); |
197 |
197 |
198 |
198 |
199 (* atomize *) |
199 (* atomize *) |
200 |
200 |
201 fun atomize_term thy = |
201 fun atomize_term thy = |