1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -27,8 +27,8 @@
     1.4  
     1.5  ML \<open>
     1.6  val inverse_z = prep_rls'(
     1.7 -  Rule_Set.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
     1.8 -	  erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
     1.9 +  Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.10 +	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.11  	  rules = 
    1.12  	   [
    1.13      Rule.Thm ("rule4", @{thm rule4})
    1.14 @@ -120,14 +120,14 @@
    1.15          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.16            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.17          {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [],
    1.18 -          srls = Rule_Set.Rls {id="srls_partial_fraction", 
    1.19 +          srls = Rule_Def.Repeat {id="srls_partial_fraction", 
    1.20                preconds = [], rew_ord = ("termlessI",termlessI),
    1.21                erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls
    1.22                    [(*for asm in NTH_CONS ...*)
    1.23                      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.24                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.25                      Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], 
    1.26 -              srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.27 +              srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.28                rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
    1.29                    Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.30                    Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),