1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -214,8 +214,8 @@
     1.4  
     1.5  (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
     1.6   val sqrt_isolate = prep_rls'(
     1.7 -  Rule_Set.Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), 
     1.8 -       erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
     1.9 +  Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.10 +       erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.11         rules = [
    1.12         Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1}),
    1.13                       (* (sqrt a)^^^2 -> a *)
    1.14 @@ -313,9 +313,9 @@
    1.15  \<close> ML \<open>
    1.16  (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
    1.17   val l_sqrt_isolate = prep_rls'(
    1.18 -     Rule_Set.Rls {id = "l_sqrt_isolate", preconds = [], 
    1.19 +     Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [], 
    1.20  	  rew_ord = ("termlessI",termlessI), 
    1.21 -          erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.22 +          erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.23       rules = [
    1.24       Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1}),
    1.25                              (* (sqrt a)^^^2 -> a *)
    1.26 @@ -359,9 +359,9 @@
    1.27  (* -- right 28.8.02--*)
    1.28  (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
    1.29   val r_sqrt_isolate = prep_rls'(
    1.30 -     Rule_Set.Rls {id = "r_sqrt_isolate", preconds = [], 
    1.31 +     Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [], 
    1.32  	  rew_ord = ("termlessI",termlessI), 
    1.33 -          erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.34 +          erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.35       rules = [
    1.36       Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1}),
    1.37                             (* (sqrt a)^^^2 -> a *)
    1.38 @@ -403,9 +403,9 @@
    1.39  
    1.40  \<close> ML \<open>
    1.41  val rooteq_simplify = prep_rls'(
    1.42 -  Rule_Set.Rls {id = "rooteq_simplify", 
    1.43 +  Rule_Def.Repeat {id = "rooteq_simplify", 
    1.44         preconds = [], rew_ord = ("termlessI",termlessI), 
    1.45 -       erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.46 +       erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.47         (*asm_thm = [("sqrt_square_1","")],*)
    1.48         rules = [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
    1.49                               (* a+(b+c) = a+b+c *)