1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4  
     1.5  (*.converts a term such that differentiation works optimally.*)
     1.6  val diff_conv =   
     1.7 -    Rule_Set.Rls {id="diff_conv", 
     1.8 +    Rule_Def.Repeat {id="diff_conv", 
     1.9  	 preconds = [], 
    1.10  	 rew_ord = ("termlessI",termlessI), 
    1.11  	 erls = Rule_Set.append_rls "erls_diff_conv" Rule_Set.e_rls 
    1.12 @@ -117,7 +117,7 @@
    1.13  			    Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
    1.14  			    Rule.Thm ("and_false",TermC.num_str @{thm and_false})
    1.15  			    ], 
    1.16 -	 srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.17 +	 srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.18  	 rules =
    1.19    [Rule.Thm ("frac_conv", TermC.num_str @{thm frac_conv}),
    1.20       (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b ^^^ ?n = ?a * ?b ^^^ - ?n"*)
    1.21 @@ -144,13 +144,13 @@
    1.22  ML \<open>
    1.23  (*.beautifies a term after differentiation.*)
    1.24  val diff_sym_conv =   
    1.25 -    Rule_Set.Rls {id="diff_sym_conv", 
    1.26 +    Rule_Def.Repeat {id="diff_sym_conv", 
    1.27  	 preconds = [], 
    1.28  	 rew_ord = ("termlessI",termlessI), 
    1.29  	 erls = Rule_Set.append_rls "erls_diff_sym_conv" Rule_Set.e_rls 
    1.30  			   [Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
    1.31  			    ], 
    1.32 -	 srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.33 +	 srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.34  	 rules = [Rule.Thm ("frac_sym_conv", TermC.num_str @{thm frac_sym_conv}),
    1.35  		  Rule.Thm ("sqrt_sym_conv", TermC.num_str @{thm sqrt_sym_conv}),
    1.36  		  Rule.Thm ("root_sym_conv", TermC.num_str @{thm root_sym_conv}),
    1.37 @@ -169,11 +169,11 @@
    1.38  
    1.39  (*..*)
    1.40  val srls_diff = 
    1.41 -    Rule_Set.Rls {id="srls_differentiate..", 
    1.42 +    Rule_Def.Repeat {id="srls_differentiate..", 
    1.43  	 preconds = [], 
    1.44  	 rew_ord = ("termlessI",termlessI), 
    1.45  	 erls = Rule_Set.e_rls, 
    1.46 -	 srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.47 +	 srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.48  	 rules = [Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
    1.49  		  Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_"),
    1.50  		  Rule.Num_Calc("Diff.primed", eval_primed "Diff.primed")
    1.51 @@ -195,8 +195,8 @@
    1.52  
    1.53  (*.rules for differentiation, _no_ simplification.*)
    1.54  val diff_rules =
    1.55 -    Rule_Set.Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.56 -	 erls = erls_diff, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.57 +    Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.58 +	 erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.59  	 rules = [Rule.Thm ("diff_sum",TermC.num_str @{thm diff_sum}),
    1.60  		  Rule.Thm ("diff_dif",TermC.num_str @{thm diff_dif}),
    1.61  		  Rule.Thm ("diff_prod_const",TermC.num_str @{thm diff_prod_const}),
    1.62 @@ -224,9 +224,9 @@
    1.63  ML \<open>
    1.64  (*.normalisation for checking user-input.*)
    1.65  val norm_diff = 
    1.66 -  Rule_Set.Rls
    1.67 +  Rule_Def.Repeat
    1.68      {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.69 -     erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.70 +     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.71       rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
    1.72       scr = Rule.EmptyScr};
    1.73  \<close>