1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Aug 04 15:38:42 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Aug 04 16:48:37 2022 +0200
     1.3 @@ -232,8 +232,8 @@
     1.4    	 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
     1.5    	 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
     1.6  
     1.7 -  	 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
     1.8 -  	 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
     1.9 +  	 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.10 +  	 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_"),
    1.11  
    1.12    	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
    1.13          (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
    1.14 @@ -257,7 +257,7 @@
    1.15        \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
    1.16        \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
    1.17  
    1.18 -      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    1.19 +      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
    1.20  
    1.21        \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
    1.22        \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
    1.23 @@ -316,9 +316,9 @@
    1.24    	Rule.Rls_ verschoenere];
    1.25  val rechnen = 
    1.26    Rule_Set.append_rules "rechnen" Rule_Set.empty [
    1.27 -    \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
    1.28 -    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.29 -    \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")];
    1.30 +    \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
    1.31 +    \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.32 +    \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_")];
    1.33  \<close>
    1.34  rule_set_knowledge
    1.35    ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and