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};