1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -535,7 +535,7 @@
     1.4        \emph{srls}:
     1.5  \begin{verbatim}
     1.6    val srls = 
     1.7 -    Rls{id = "srls_InverseZTransform",
     1.8 +    Rule_Set.Repeat{id = "srls_InverseZTransform",
     1.9          rules = [Num_Calc("Rational.get_numerator",
    1.10                     eval_get_numerator "Rational.get_numerator"),
    1.11                   Num_Calc("Partial_Fractions.factors_from_solution",
    1.12 @@ -698,8 +698,8 @@
    1.13         
    1.14  ML \<open>
    1.15    val ansatz_rls = prep_rls @{theory} (
    1.16 -    Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
    1.17 -      erls = e_rls, srls = Erls, calc = [], errpatts = [],
    1.18 +    Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
    1.19 +      erls = e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.20        rules = [
    1.21          Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
    1.22          Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
    1.23 @@ -1085,7 +1085,7 @@
    1.24  
    1.25  ML \<open>
    1.26    val srls = 
    1.27 -    Rls {id="srls_InverseZTransform", 
    1.28 +    Rule_Set.Repeat {id="srls_InverseZTransform", 
    1.29           preconds = [],
    1.30           rew_ord = ("termlessI",termlessI),
    1.31           erls = append_rls "erls_in_srls_InverseZTransform" e_rls
    1.32 @@ -1094,7 +1094,7 @@
    1.33              (*2nd NTH_CONS pushes n+-1 into asms*)
    1.34              Num_Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.35             ], 
    1.36 -         srls = Erls, calc = [], errpatts = [],
    1.37 +         srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.38           rules = [
    1.39                    Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.40                    Num_Calc("Groups.plus_class.plus", eval_binop "#add_"),