test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 59773 d88bb023c380
parent 59717 cc83c55e1c1c
child 59845 273ffde50058
     1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -536,9 +536,9 @@
     1.4  \begin{verbatim}
     1.5    val srls = 
     1.6      Rls{id = "srls_InverseZTransform",
     1.7 -        rules = [Calc("Rational.get_numerator",
     1.8 +        rules = [Num_Calc("Rational.get_numerator",
     1.9                     eval_get_numerator "Rational.get_numerator"),
    1.10 -                 Calc("Partial_Fractions.factors_from_solution",
    1.11 +                 Num_Calc("Partial_Fractions.factors_from_solution",
    1.12                     eval_factors_from_solution 
    1.13                       "Partial_Fractions.factors_from_solution")]}
    1.14  \end{verbatim}                
    1.15 @@ -1090,23 +1090,23 @@
    1.16           rew_ord = ("termlessI",termlessI),
    1.17           erls = append_rls "erls_in_srls_InverseZTransform" e_rls
    1.18             [(*for asm in NTH_CONS ...*)
    1.19 -            Calc ("Orderings.ord_class.less",eval_equ "#less_"),
    1.20 +            Num_Calc ("Orderings.ord_class.less",eval_equ "#less_"),
    1.21              (*2nd NTH_CONS pushes n+-1 into asms*)
    1.22 -            Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.23 +            Num_Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.24             ], 
    1.25           srls = Erls, calc = [], errpatts = [],
    1.26           rules = [
    1.27                    Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.28 -                  Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.29 +                  Num_Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.30                    Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.31 -                  Calc("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.32 -                  Calc("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
    1.33 -                  Calc("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
    1.34 -                  Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.35 -                  Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.36 -                  Calc("Partial_Fractions.factors_from_solution",
    1.37 +                  Num_Calc("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.38 +                  Num_Calc("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
    1.39 +                  Num_Calc("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
    1.40 +                  Num_Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.41 +                  Num_Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.42 +                  Num_Calc("Partial_Fractions.factors_from_solution",
    1.43                         eval_factors_from_solution "#factors_from_solution"),
    1.44 -                  Calc("Partial_Fractions.drop_questionmarks",
    1.45 +                  Num_Calc("Partial_Fractions.drop_questionmarks",
    1.46                         eval_drop_questionmarks "#drop_?")
    1.47                   ],
    1.48           scr = EmptyScr};