161 rew_ord = ("termlessI",termlessI), |
161 rew_ord = ("termlessI",termlessI), |
162 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty |
162 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty |
163 [(*for asm in NTH_CONS ...*) |
163 [(*for asm in NTH_CONS ...*) |
164 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
164 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
165 (*2nd NTH_CONS pushes n+-1 into asms*) |
165 (*2nd NTH_CONS pushes n+-1 into asms*) |
166 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
166 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], |
167 srls = Rule_Set.Empty, calc = [], errpatts = [], |
167 srls = Rule_Set.Empty, calc = [], errpatts = [], |
168 rules = [ |
168 rules = [ |
169 \<^rule_thm>\<open>NTH_CONS\<close>, |
169 \<^rule_thm>\<open>NTH_CONS\<close>, |
170 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
170 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
171 \<^rule_thm>\<open>NTH_NIL\<close>, |
171 \<^rule_thm>\<open>NTH_NIL\<close>, |
172 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"), |
172 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"), |
173 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"), |
173 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"), |
174 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"), |
174 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"), |
175 \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"), |
175 \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"), |