src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
changeset 60515 03e19793d81e
parent 60509 2e0b7ca391dc
child 60586 007ef64dbb08
     1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Aug 04 15:38:42 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Aug 04 16:48:37 2022 +0200
     1.3 @@ -115,10 +115,10 @@
     1.4        erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
     1.5          \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*)
     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 = [\<^rule_thm>\<open>NTH_CONS\<close>,
    1.11 -        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.12 +        \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.13          \<^rule_thm>\<open>NTH_NIL\<close>,
    1.14          \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
    1.15          \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),