1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Aug 29 13:52:47 2019 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue Sep 03 12:40:27 2019 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5  subsubsection \<open>Get the Argument of the Expression X'\<close>
     1.6  text\<open>\noindent We use \texttt{grep} for finding possibilities how we can
     1.7 -       extract the bound variable in the expression. \ttfamily Atools.thy, 
     1.8 +       extract the bound variable in the expression. \ttfamily Prog_Expr.thy, 
     1.9         Tools.thy \normalfont contain general utilities: \ttfamily 
    1.10         eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
    1.11         \ttfamily grep -r "fun eva\_" * \normalfont shows all functions 
    1.12 @@ -1097,20 +1097,15 @@
    1.13           srls = Erls, calc = [], errpatts = [],
    1.14           rules = [
    1.15                    Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.16 -                  Calc("Groups.plus_class.plus", 
    1.17 -                       eval_binop "#add_"),
    1.18 +                  Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.19                    Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.20 -                  Calc("Tools.lhs", eval_lhs"eval_lhs_"),
    1.21 -                  Calc("Tools.rhs", eval_rhs"eval_rhs_"),
    1.22 -                  Calc("Atools.argument'_in",
    1.23 -                       eval_argument_in "Atools.argument'_in"),
    1.24 -                  Calc("Rational.get_denominator",
    1.25 -                       eval_get_denominator "#get_denominator"),
    1.26 -                  Calc("Rational.get_numerator",
    1.27 -                       eval_get_numerator "#get_numerator"),
    1.28 +                  Calc("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
    1.29 +                  Calc("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
    1.30 +                  Calc("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"),
    1.31 +                  Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
    1.32 +                  Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
    1.33                    Calc("Partial_Fractions.factors_from_solution",
    1.34 -                       eval_factors_from_solution 
    1.35 -                         "#factors_from_solution"),
    1.36 +                       eval_factors_from_solution "#factors_from_solution"),
    1.37                    Calc("Partial_Fractions.drop_questionmarks",
    1.38                         eval_drop_questionmarks "#drop_?")
    1.39                   ],