404 \<^rule_thm>\<open>real_assoc_1\<close>, |
404 \<^rule_thm>\<open>real_assoc_1\<close>, |
405 \<^rule_thm>\<open>real_assoc_2\<close>, |
405 \<^rule_thm>\<open>real_assoc_2\<close>, |
406 \<^rule_thm>\<open>real_diff_minus\<close>, |
406 \<^rule_thm>\<open>real_diff_minus\<close>, |
407 \<^rule_thm>\<open>real_unari_minus\<close>, |
407 \<^rule_thm>\<open>real_unari_minus\<close>, |
408 \<^rule_thm>\<open>realpow_multI\<close>, |
408 \<^rule_thm>\<open>realpow_multI\<close>, |
409 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
409 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
410 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), |
410 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
411 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
411 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
412 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
412 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
413 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
413 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
414 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
414 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
415 Rule.Rls_ reduce_012], |
415 Rule.Rls_ reduce_012], |
416 scr = Rule.Empty_Prog}); |
416 scr = Rule.Empty_Prog}); |
417 \<close> |
417 \<close> |
418 rule_set_knowledge |
418 rule_set_knowledge |
419 cancel_leading_coeff = cancel_leading_coeff and |
419 cancel_leading_coeff = cancel_leading_coeff and |