test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 60516 795d1352493a
parent 60495 54642eaf7bba
child 60558 2350ba2640fd
     1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Aug 04 16:48:37 2022 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri Aug 05 08:45:37 2022 +0200
     1.3 @@ -1096,12 +1096,12 @@
     1.4             [(*for asm in NTH_CONS ...*)
     1.5              Eval (\<^const_name>\<open>less\<close>,eval_equ "#less_"),
     1.6              (*2nd NTH_CONS pushes n+-1 into asms*)
     1.7 -            Eval(\<^const_name>\<open>plus\<close>, eval_binop "#add_")
     1.8 +            Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")
     1.9             ], 
    1.10           srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.11           rules = [
    1.12                    Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
    1.13 -                  Eval(\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
    1.14 +                  Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
    1.15                    Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
    1.16                    Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.17                    Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),