src/Tools/isac/Knowledge/Partial_Fractions.thy
changeset 60515 03e19793d81e
parent 60509 2e0b7ca391dc
child 60586 007ef64dbb08
     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_"),