equal
deleted
inserted
replaced
511 |
511 |
512 (**)in(**) |
512 (**)in(**) |
513 |
513 |
514 val cancel_p = |
514 val cancel_p = |
515 Rule_Set.Rrls {id = "cancel_p", prepat = [], |
515 Rule_Set.Rrls {id = "cancel_p", prepat = [], |
516 rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
516 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
517 erls = rational_erls, |
517 erls = rational_erls, |
518 calc = |
518 calc = |
519 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
519 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
520 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
520 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
521 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
521 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |