1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 04 15:38:42 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 04 16:48:37 2022 +0200
1.3 @@ -163,11 +163,11 @@
1.4 [(*for asm in NTH_CONS ...*)
1.5 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.6 (*2nd NTH_CONS pushes n+-1 into asms*)
1.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
1.8 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
1.9 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.10 rules = [
1.11 \<^rule_thm>\<open>NTH_CONS\<close>,
1.12 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.13 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.14 \<^rule_thm>\<open>NTH_NIL\<close>,
1.15 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
1.16 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),