equal
deleted
inserted
replaced
547 |
547 |
548 fun ord_make_polynomial (pr:bool) thy (_: subst) (ts, us) = |
548 fun ord_make_polynomial (pr:bool) thy (_: subst) (ts, us) = |
549 (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); |
549 (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); |
550 |
550 |
551 end;(*local*) |
551 end;(*local*) |
552 |
552 \<close> |
553 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *) |
553 setup \<open>KEStore_Elems.add_rew_ord [ |
554 [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]); |
554 ("termlessI", termlessI), |
555 \<close> |
555 ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]\<close> |
556 |
556 |
557 subsection \<open>predicates\<close> |
557 subsection \<open>predicates\<close> |
558 subsubsection \<open>in specifications\<close> |
558 subsubsection \<open>in specifications\<close> |
559 ML \<open> |
559 ML \<open> |
560 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
560 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |