equal
deleted
inserted
replaced
17 (* atomize_elim rules *) |
17 (* atomize_elim rules *) |
18 |
18 |
19 val named_theorems = |
19 val named_theorems = |
20 Context.>>> (Context.map_theory_result |
20 Context.>>> (Context.map_theory_result |
21 (Named_Target.theory_init #> |
21 (Named_Target.theory_init #> |
22 Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> [] "atomize_elim rewrite rule" ##> |
22 Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> "atomize_elim rewrite rule" ##> |
23 Local_Theory.exit_global)); |
23 Local_Theory.exit_global)); |
24 |
24 |
25 |
25 |
26 (* More conversions: *) |
26 (* More conversions: *) |
27 local open Conv in |
27 local open Conv in |