1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jan 17 12:37:21 2020 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jan 17 13:14:11 2020 +0100
1.3 @@ -124,19 +124,19 @@
1.4 preconds = [], rew_ord = ("termlessI",termlessI),
1.5 erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls
1.6 [(*for asm in NTH_CONS ...*)
1.7 - Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.8 + Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.9 (*2nd NTH_CONS pushes n+-1 into asms*)
1.10 - Rule.Calc("Groups.plus_class.plus", (**)eval_binop "#add_")],
1.11 + Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")],
1.12 srls = Rule.Erls, calc = [], errpatts = [],
1.13 rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
1.14 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.15 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.16 Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
1.17 - Rule.Calc ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
1.18 - Rule.Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
1.19 - Rule.Calc ("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
1.20 - Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.21 - Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.22 - Rule.Calc ("Partial_Fractions.factors_from_solution",
1.23 + Rule.Num_Calc ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
1.24 + Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
1.25 + Rule.Num_Calc ("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
1.26 + Rule.Num_Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.27 + Rule.Num_Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.28 + Rule.Num_Calc ("Partial_Fractions.factors_from_solution",
1.29 eval_factors_from_solution "#factors_from_solution")
1.30 ], scr = Rule.EmptyScr},
1.31 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},