1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Thu Aug 04 15:38:42 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Aug 04 16:48:37 2022 +0200
     1.3 @@ -406,12 +406,12 @@
     1.4    		\<^rule_thm>\<open>real_diff_minus\<close>,
     1.5    		\<^rule_thm>\<open>real_unari_minus\<close>,
     1.6    		\<^rule_thm>\<open>realpow_multI\<close>,
     1.7 -  		\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
     1.8 -  		\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
     1.9 -  		\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    1.10 +  		\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.11 +  		\<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
    1.12 +  		\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
    1.13    		\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.14    		\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    1.15 -  		\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    1.16 +  		\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
    1.17         Rule.Rls_ reduce_012],
    1.18      scr = Rule.Empty_Prog});
    1.19  \<close>