113 srls = Rule_Def.Repeat { |
113 srls = Rule_Def.Repeat { |
114 id = "srls_partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), |
114 id = "srls_partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), |
115 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [ |
115 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [ |
116 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*) |
116 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*) |
117 (*2nd NTH_CONS pushes n+-1 into asms*) |
117 (*2nd NTH_CONS pushes n+-1 into asms*) |
118 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
118 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], |
119 srls = Rule_Set.Empty, calc = [], errpatts = [], |
119 srls = Rule_Set.Empty, calc = [], errpatts = [], |
120 rules = [\<^rule_thm>\<open>NTH_CONS\<close>, |
120 rules = [\<^rule_thm>\<open>NTH_CONS\<close>, |
121 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
121 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
122 \<^rule_thm>\<open>NTH_NIL\<close>, |
122 \<^rule_thm>\<open>NTH_NIL\<close>, |
123 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"), |
123 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"), |
124 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"), |
124 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"), |
125 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"), |
125 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"), |
126 \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"), |
126 \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"), |