1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Jun 10 17:06:32 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Fri Jun 11 11:49:34 2021 +0200
     1.3 @@ -122,20 +122,19 @@
     1.4                preconds = [], rew_ord = ("termlessI",termlessI),
     1.5                erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
     1.6                    [(*for asm in NTH_CONS ...*)
     1.7 -                    Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
     1.8 +                    \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
     1.9                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.10 -                    Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")], 
    1.11 +                    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
    1.12                srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.13                rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
    1.14 -                  Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.15 +                  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.16                    Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
    1.17 -                  Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
    1.18 -                  Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
    1.19 -                  Rule.Eval ("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
    1.20 -                  Rule.Eval ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.21 -                  Rule.Eval ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.22 -                  Rule.Eval ("Partial_Fractions.factors_from_solution",
    1.23 -                    eval_factors_from_solution "#factors_from_solution")
    1.24 +                  \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
    1.25 +                  \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
    1.26 +                  \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
    1.27 +                  \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
    1.28 +                  \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
    1.29 +                  \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
    1.30                    ], scr = Rule.Empty_Prog},
    1.31            prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
    1.32          @{thm inverse_ztransform2.simps})]