1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Aug 04 15:38:42 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Aug 04 16:48:37 2022 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4      (*		
     1.5       Don't use
     1.6       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
     1.7 -     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
     1.8 +     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     1.9       *)
    1.10      ];
    1.11  
    1.12 @@ -57,7 +57,7 @@
    1.13      (*		
    1.14       Don't use
    1.15       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.16 -     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    1.17 +     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
    1.18       *)
    1.19      ];
    1.20  \<close>
    1.21 @@ -72,14 +72,14 @@
    1.22      calc = [], errpatts = [],
    1.23      rules = [
    1.24        \<^rule_thm>\<open>real_assoc_1\<close>,
    1.25 -      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.26 -      \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
    1.27 -      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    1.28 +      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.29 +      \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
    1.30 +      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
    1.31        (*  Don't use  
    1.32         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.33         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    1.34         *)
    1.35 -      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
    1.36 +      \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
    1.37      scr = Rule.Empty_Prog});
    1.38  \<close>
    1.39  rule_set_knowledge LinPoly_simplify = LinPoly_simplify