equal
deleted
inserted
replaced
52 \<close> ML \<open> |
52 \<close> ML \<open> |
53 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*) |
53 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*) |
54 val tless_true = Rewrite_Ord.function_empty; |
54 val tless_true = Rewrite_Ord.function_empty; |
55 \<close> ML \<open> |
55 \<close> ML \<open> |
56 \<close> |
56 \<close> |
57 setup \<open>KEStore_Elems.add_rew_ord [ |
57 setup \<open>KEStore_Elems.add_rew_ords [ |
58 ("tless_true", tless_true), |
58 ("tless_true", tless_true), |
59 ("Rewrite_Ord.id_empty", tless_true), |
59 ("Rewrite_Ord.id_empty", tless_true), |
60 ("e_rew_ord'", tless_true), |
60 ("e_rew_ord'", tless_true), |
61 ("dummy_ord", Rewrite_Ord.function_empty)]\<close> |
61 ("dummy_ord", Rewrite_Ord.function_empty)]\<close> |
62 |
62 |