equal
deleted
inserted
replaced
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.e_rew_ord = Rewrite_Ord.dummy_ord*) |
54 val tless_true = Rewrite_Ord.dummy_ord; |
54 val tless_true = Rewrite_Ord.dummy_ord; |
55 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*) |
55 \<close> ML \<open> |
56 [("tless_true", tless_true), |
56 \<close> |
57 ("e_rew_ord'", tless_true), |
57 setup \<open>KEStore_Elems.add_rew_ord [ |
58 ("dummy_ord", Rewrite_Ord.dummy_ord)]); |
58 ("tless_true", tless_true), |
59 \<close> |
59 ("e_rew_ord", tless_true), |
|
60 ("e_rew_ord'", tless_true), |
|
61 ("dummy_ord", Rewrite_Ord.dummy_ord)]\<close> |
60 |
62 |
61 subsection \<open>rule-sets\<close> |
63 subsection \<open>rule-sets\<close> |
62 ML \<open> |
64 ML \<open> |
63 \<close> ML \<open> |
65 \<close> ML \<open> |
64 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 [ |