1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -169,8 +169,8 @@
     1.4  	      Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
     1.5  		  (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], 
     1.6  		       rew_ord = ("dummy_ord",Rule.dummy_ord), 
     1.7 -		       erls = (*FIXME.WN051028 Rule_Set.e_rls,*)
     1.8 -		       Rule_Set.append_rls "Rule_Set.e_rls-is_polyexp" Rule_Set.e_rls
     1.9 +		       erls = (*FIXME.WN051028 Rule_Set.empty,*)
    1.10 +		       Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
    1.11  				  [Rule.Num_Calc ("Poly.is'_polyexp", 
    1.12  					 eval_is_polyexp "")],
    1.13  				  srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.14 @@ -226,7 +226,7 @@
    1.15     *1* expand the term, ie. distribute * and / over +
    1.16  .*)
    1.17  val separate_bdv2 =
    1.18 -    Rule_Set.append_rls "separate_bdv2"
    1.19 +    Rule_Set.append_rules "separate_bdv2"
    1.20  	       collect_bdv
    1.21  	       [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
    1.22  		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
    1.23 @@ -279,7 +279,7 @@
    1.24  * 	       Rule.Rls_ discard_parentheses,
    1.25  * 	       Rule.Rls_ collect_bdv,
    1.26  * 	       (*below inserted from 'make_ratpoly_in'*)
    1.27 -* 	       Rule.Rls_ (Rule_Set.append_rls "separate_bdv"
    1.28 +* 	       Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
    1.29  * 			 collect_bdv
    1.30  * 			 [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
    1.31  * 			  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
    1.32 @@ -335,7 +335,7 @@
    1.33        (["integrate","function"],
    1.34          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.35            ("#Find"  ,["antiDerivative F_F"])],
    1.36 -        Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], 
    1.37 +        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.38          SOME "Integrate (f_f, v_v)", 
    1.39          [["diff","integration"]])),
    1.40      (*here "named" is used differently from Differentiation"*)
    1.41 @@ -343,7 +343,7 @@
    1.42        (["named","integrate","function"],
    1.43          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.44            ("#Find"  ,["antiDerivativeName F_F"])],
    1.45 -        Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], 
    1.46 +        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.47          SOME "Integrate (f_f, v_v)", 
    1.48          [["diff","integration","named"]]))]\<close>
    1.49  
    1.50 @@ -360,8 +360,8 @@
    1.51      [Specify.prep_met thy "met_diffint" [] Celem.e_metID
    1.52  	    (["diff","integration"],
    1.53  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.54 -	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls,
    1.55 -	        crls = Atools_erls, errpats = [], nrls = Rule_Set.e_rls},
    1.56 +	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.57 +	        crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.58  	      @{thm integrate.simps})]
    1.59  \<close>
    1.60  
    1.61 @@ -379,8 +379,8 @@
    1.62  	    (["diff","integration","named"],
    1.63  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.64  	        ("#Find"  ,["antiDerivativeName F_F"])],
    1.65 -	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls,
    1.66 -          crls = Atools_erls, errpats = [], nrls = Rule_Set.e_rls},
    1.67 +	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.68 +          crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.69          @{thm intergrate_named.simps})]
    1.70  \<close>
    1.71