src/Tools/isac/Knowledge/Integrate.thy
changeset 60515 03e19793d81e
parent 60509 2e0b7ca391dc
child 60586 007ef64dbb08
     1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 15:38:42 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 16:48:37 2022 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4     	  \<^rule_thm>\<open>integral_add\<close>,
     1.5     	  \<^rule_thm>\<open>integral_mult\<close>,
     1.6     	  \<^rule_thm>\<open>integral_pow\<close>,
     1.7 -   	  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)],
     1.8 +   	  \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)],
     1.9      scr = Rule.Empty_Prog};
    1.10  \<close>
    1.11  ML \<open>