1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -536,9 +536,9 @@
     1.4  \begin{verbatim}
     1.5    val srls = 
     1.6      Rule_Set.Repeat{id = "srls_InverseZTransform",
     1.7 -        rules = [Num_Calc("Rational.get_numerator",
     1.8 +        rules = [Eval("Rational.get_numerator",
     1.9                     eval_get_numerator "Rational.get_numerator"),
    1.10 -                 Num_Calc("Partial_Fractions.factors_from_solution",
    1.11 +                 Eval("Partial_Fractions.factors_from_solution",
    1.12                     eval_factors_from_solution 
    1.13                       "Partial_Fractions.factors_from_solution")]}
    1.14  \end{verbatim}                
    1.15 @@ -704,7 +704,7 @@
    1.16          Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
    1.17          Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order})
    1.18                ], 
    1.19 -      scr = EmptyScr});
    1.20 +      scr = Empty_Prog});
    1.21  \<close>
    1.22  
    1.23  text\<open>\noindent We apply the ruleset\ldots\<close>
    1.24 @@ -1090,26 +1090,26 @@
    1.25           rew_ord = ("termlessI",termlessI),
    1.26           erls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
    1.27             [(*for asm in NTH_CONS ...*)
    1.28 -            Num_Calc ("Orderings.ord_class.less",eval_equ "#less_"),
    1.29 +            Eval ("Orderings.ord_class.less",eval_equ "#less_"),
    1.30              (*2nd NTH_CONS pushes n+-1 into asms*)
    1.31 -            Num_Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.32 +            Eval("Groups.plus_class.plus", eval_binop "#add_")
    1.33             ], 
    1.34           srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.35           rules = [
    1.36                    Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
    1.37 -                  Num_Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.38 +                  Eval("Groups.plus_class.plus", eval_binop "#add_"),
    1.39                    Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
    1.40 -                  Num_Calc("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.41 -                  Num_Calc("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
    1.42 -                  Num_Calc("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
    1.43 -                  Num_Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.44 -                  Num_Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.45 -                  Num_Calc("Partial_Fractions.factors_from_solution",
    1.46 +                  Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.47 +                  Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
    1.48 +                  Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
    1.49 +                  Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.50 +                  Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.51 +                  Eval("Partial_Fractions.factors_from_solution",
    1.52                         eval_factors_from_solution "#factors_from_solution"),
    1.53 -                  Num_Calc("Partial_Fractions.drop_questionmarks",
    1.54 +                  Eval("Partial_Fractions.drop_questionmarks",
    1.55                         eval_drop_questionmarks "#drop_?")
    1.56                   ],
    1.57 -         scr = EmptyScr};
    1.58 +         scr = Empty_Prog};
    1.59  \<close>
    1.60  
    1.61