equal
deleted
inserted
replaced
128 \<^rule_thm>\<open>integral_const\<close>, |
128 \<^rule_thm>\<open>integral_const\<close>, |
129 \<^rule_thm>\<open>integral_var\<close>, |
129 \<^rule_thm>\<open>integral_var\<close>, |
130 \<^rule_thm>\<open>integral_add\<close>, |
130 \<^rule_thm>\<open>integral_add\<close>, |
131 \<^rule_thm>\<open>integral_mult\<close>, |
131 \<^rule_thm>\<open>integral_mult\<close>, |
132 \<^rule_thm>\<open>integral_pow\<close>, |
132 \<^rule_thm>\<open>integral_pow\<close>, |
133 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)], |
133 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)], |
134 scr = Rule.Empty_Prog}; |
134 scr = Rule.Empty_Prog}; |
135 \<close> |
135 \<close> |
136 ML \<open> |
136 ML \<open> |
137 val add_new_c = |
137 val add_new_c = |
138 Rule_Set.Sequence {id="add_new_c", preconds = [], |
138 Rule_Set.Sequence {id="add_new_c", preconds = [], |