1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Aug 04 15:38:42 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Aug 04 16:48:37 2022 +0200
     1.3 @@ -324,14 +324,14 @@
     1.4        erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.5        rules = [(*for precond NTH_CONS ...*)
     1.6           \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
     1.7 -         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
     1.8 +         \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
     1.9           \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
    1.10           (*immediately repeated rewrite pushes '+' into precondition !*)
    1.11        scr = Rule.Empty_Prog}, 
    1.12      srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.13      rules = [
    1.14        \<^rule_thm>\<open>NTH_CONS\<close>,
    1.15 -      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.16 +      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.17        \<^rule_thm>\<open>NTH_NIL\<close>,
    1.18        \<^rule_thm>\<open>tl_Cons\<close>,
    1.19        \<^rule_thm>\<open>tl_Nil\<close>,
    1.20 @@ -350,13 +350,13 @@
    1.21      erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.22      rules = [(*for precond NTH_CONS ...*)
    1.23    	   \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.24 -  	   \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
    1.25 +  	   \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
    1.26    	   (*immediately repeated rewrite pushes '+' into precondition !*)
    1.27      scr = Rule.Empty_Prog}, 
    1.28    srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.29    rules = [
    1.30      \<^rule_thm>\<open>NTH_CONS\<close>,
    1.31 -    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.32 +    \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.33      \<^rule_thm>\<open>NTH_NIL\<close>,
    1.34      \<^rule_thm>\<open>tl_Cons\<close>,
    1.35      \<^rule_thm>\<open>tl_Nil\<close>,
    1.36 @@ -394,7 +394,7 @@
    1.37    \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty 
    1.38      [\<^rule_thm>\<open>LENGTH_CONS\<close>,
    1.39        \<^rule_thm>\<open>LENGTH_NIL\<close>,
    1.40 -      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.41 +      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.42        \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
    1.43    CAS: "solveSystem e_s v_s"
    1.44    Given: "equalities e_s" "solveForVars v_s"
    1.45 @@ -422,7 +422,7 @@
    1.46    \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty 
    1.47      [\<^rule_thm>\<open>LENGTH_CONS\<close>,
    1.48        \<^rule_thm>\<open>LENGTH_NIL\<close>,
    1.49 -      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.50 +      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.51        \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
    1.52    CAS: "solveSystem e_s v_s"
    1.53    Given: "equalities e_s" "solveForVars v_s"
    1.54 @@ -433,7 +433,7 @@
    1.55    \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty 
    1.56      [\<^rule_thm>\<open>LENGTH_CONS\<close>,
    1.57        \<^rule_thm>\<open>LENGTH_NIL\<close>,
    1.58 -      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.59 +      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.60        \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
    1.61    CAS: "solveSystem e_s v_s"
    1.62    Given: "equalities e_s" "solveForVars v_s"
    1.63 @@ -470,11 +470,11 @@
    1.64  				  [(*for asm in NTH_CONS ...*)
    1.65  				   \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.66  				   (*2nd NTH_CONS pushes n+-1 into asms*)
    1.67 -				   \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
    1.68 +				   \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")
    1.69  				   ], 
    1.70  		srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.71  		rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
    1.72 -			 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.73 +			 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.74  			 \<^rule_thm>\<open>NTH_NIL\<close>],
    1.75  		scr = Rule.Empty_Prog};
    1.76  \<close>