1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  	   [
     1.5      Rule.Thm ("rule4", @{thm rule4})
     1.6  	   ], 
     1.7 -	 scr = Rule.EmptyScr});
     1.8 +	 scr = Rule.Empty_Prog});
     1.9  \<close>
    1.10  
    1.11  
    1.12 @@ -124,21 +124,21 @@
    1.13                preconds = [], rew_ord = ("termlessI",termlessI),
    1.14                erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
    1.15                    [(*for asm in NTH_CONS ...*)
    1.16 -                    Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.17 +                    Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.18                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.19 -                    Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], 
    1.20 +                    Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")], 
    1.21                srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.22                rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
    1.23 -                  Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.24 +                  Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.25                    Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
    1.26 -                  Rule.Num_Calc ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
    1.27 -                  Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
    1.28 -                  Rule.Num_Calc ("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
    1.29 -                  Rule.Num_Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.30 -                  Rule.Num_Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.31 -                  Rule.Num_Calc ("Partial_Fractions.factors_from_solution",
    1.32 +                  Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
    1.33 +                  Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
    1.34 +                  Rule.Eval ("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
    1.35 +                  Rule.Eval ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.36 +                  Rule.Eval ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.37 +                  Rule.Eval ("Partial_Fractions.factors_from_solution",
    1.38                      eval_factors_from_solution "#factors_from_solution")
    1.39 -                  ], scr = Rule.EmptyScr},
    1.40 +                  ], scr = Rule.Empty_Prog},
    1.41            prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
    1.42          @{thm inverse_ztransform2.simps})]
    1.43  \<close>