equal
deleted
inserted
replaced
157 (term_ord' pr thy (Library.swap tu) = LESS);*) |
157 (term_ord' pr thy (Library.swap tu) = LESS);*) |
158 |
158 |
159 (*for the rls's*) |
159 (*for the rls's*) |
160 fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = |
160 fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = |
161 (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS); |
161 (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS); |
162 (**) |
162 |
163 end; |
163 (**)end;(**) |
164 (**) |
164 \<close> ML \<open> |
165 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', |
165 \<close> |
166 [("ord_simplify_System", ord_simplify_System false \<^theory>) |
166 setup \<open>KEStore_Elems.add_rew_ord [ |
167 ]); |
167 ("ord_simplify_System", ord_simplify_System false \<^theory>)]\<close> |
168 \<close> |
168 |
169 ML \<open> |
169 ML \<open> |
170 (** rulesets **) |
170 (** rulesets **) |
171 |
171 |
172 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*) |
172 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*) |
173 val order_add_mult_System = |
173 val order_add_mult_System = |