1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -73,19 +73,22 @@
     1.4  text\<open>\noindent We try to apply the rules to a given expression.\<close>
     1.5  
     1.6  ML \<open>
     1.7 -  val inverse_Z = Rule_Set.append_rules "inverse_Z" Rule_Set.empty
     1.8 -    [ Thm  ("rule3",ThmC.numerals_to_Free @{thm rule3}),
     1.9 -      Thm  ("rule4",ThmC.numerals_to_Free @{thm rule4}),
    1.10 -      Thm  ("rule1",ThmC.numerals_to_Free @{thm rule1})   
    1.11 +  val inverse_Z = Rule_Set.append_rules "inverse_Z" Atools_erls
    1.12 +    [ Rule.Thm  ("rule3",ThmC.numerals_to_Free @{thm rule3}),
    1.13 +      Rule.Thm  ("rule4",ThmC.numerals_to_Free @{thm rule4}),
    1.14 +      Rule.Thm  ("rule1",ThmC.numerals_to_Free @{thm rule1})   
    1.15      ];
    1.16  
    1.17 +\<close> ML \<open>
    1.18    val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
    1.19 +\<close> ML \<open>
    1.20    val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
    1.21    UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
    1.22    (*
    1.23     * Attention rule1 is applied before the expression is 
    1.24     * checked for rule4 which would be correct!!!
    1.25     *)
    1.26 +\<close> ML \<open>
    1.27  \<close>
    1.28  
    1.29  ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>