1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -102,14 +102,14 @@
     1.4    let
     1.5      X = Take X_eq;
     1.6      X' = Rewrite ''ruleZY''  X;
     1.7 -    X'_z = lhs X';
     1.8 -    zzz = argument_in X'_z;
     1.9 +    X_z = lhs X';
    1.10 +    zzz = argument_in X_z;
    1.11      funterm = rhs X';
    1.12      pbz = SubProblem (''Isac_Knowledge'',
    1.13          [''partial_fraction'',''rational'',''simplification''],
    1.14          [''simplification'',''of_rationals'',''to_partial_fraction''])
    1.15        [REAL funterm, REAL zzz];
    1.16 -    pbz_eq = Take (X'_z = pbz);
    1.17 +    pbz_eq = Take (X_z = pbz);
    1.18      pbz_eq = Rewrite ''ruleYZ''  pbz_eq;
    1.19      X_zeq = Take (X_z = rhs pbz_eq);
    1.20      n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
    1.21 @@ -133,7 +133,7 @@
    1.22                    Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
    1.23                    Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
    1.24                    Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
    1.25 -                  Rule.Eval ("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
    1.26 +                  Rule.Eval ("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
    1.27                    Rule.Eval ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.28                    Rule.Eval ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.29                    Rule.Eval ("Partial_Fractions.factors_from_solution",
    1.30 @@ -144,6 +144,7 @@
    1.31  \<close>
    1.32  ML \<open>
    1.33  \<close> ML \<open>
    1.34 +\<close> ML \<open>
    1.35  \<close>
    1.36  
    1.37  end