48 in |
48 in |
49 fun termlessI (_: subst) uv = LibraryC.termless uv; |
49 fun termlessI (_: subst) uv = LibraryC.termless uv; |
50 fun term_ordI (_: subst) uv = Term_Ord.term_ord uv; |
50 fun term_ordI (_: subst) uv = Term_Ord.term_ord uv; |
51 end; |
51 end; |
52 \<close> ML \<open> |
52 \<close> ML \<open> |
53 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*) |
53 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*) |
54 val tless_true = Rewrite_Ord.dummy_ord; |
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_ord [ |
58 ("tless_true", tless_true), |
58 ("tless_true", tless_true), |
59 ("e_rew_ord", 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.dummy_ord)]\<close> |
61 ("dummy_ord", Rewrite_Ord.function_empty)]\<close> |
62 |
62 |
63 subsection \<open>rule-sets\<close> |
63 subsection \<open>rule-sets\<close> |
64 ML \<open> |
64 ML \<open> |
65 \<close> ML \<open> |
65 \<close> ML \<open> |
66 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty [ |
66 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty [ |