1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Apr 08 16:56:47 2020 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4  (**)
     1.5  end;
     1.6  (**)
     1.7 -Rule.rew_ord' := overwritel (! Rule.rew_ord',
     1.8 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
     1.9  [("ord_simplify_System", ord_simplify_System false thy)
    1.10   ]);
    1.11  \<close>
    1.12 @@ -195,7 +195,7 @@
    1.13    #2 NOT using common_nominator_p                          .*)
    1.14  val norm_System_noadd_fractions = 
    1.15    Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [], 
    1.16 -       rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.17 +       rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.18         erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.19         rules = [(*sequence given by operator precedence*)
    1.20  		Rule.Rls_ discard_minus,
    1.21 @@ -216,7 +216,7 @@
    1.22    *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
    1.23  val norm_System = 
    1.24    Rule_Def.Repeat {id = "norm_System", preconds = [], 
    1.25 -       rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.26 +       rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.27         erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.28         rules = [(*sequence given by operator precedence*)
    1.29  		Rule.Rls_ discard_minus,
    1.30 @@ -244,7 +244,7 @@
    1.31     analoguous to simplify_Integral                                       .*)
    1.32  val simplify_System_parenthesized = 
    1.33    Rule_Set.Seqence {id = "simplify_System_parenthesized", preconds = []:term list, 
    1.34 -       rew_ord = ("dummy_ord", Rule.dummy_ord),
    1.35 +       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.36        erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.37        rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
    1.38   	       (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
    1.39 @@ -269,7 +269,7 @@
    1.40  (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
    1.41  val simplify_System = 
    1.42    Rule_Set.Seqence {id = "simplify_System", preconds = []:term list, 
    1.43 -       rew_ord = ("dummy_ord", Rule.dummy_ord),
    1.44 +       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.45        erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.46        rules = [Rule.Rls_ norm_Rational,
    1.47  	       Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
    1.48 @@ -289,7 +289,7 @@
    1.49  ML \<open>
    1.50  val isolate_bdvs = 
    1.51      Rule_Def.Repeat {id="isolate_bdvs", preconds = [], 
    1.52 -	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
    1.53 +	 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.54  	 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty 
    1.55  			   [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in", 
    1.56  				   eval_occur_exactly_in 
    1.57 @@ -305,7 +305,7 @@
    1.58  ML \<open>
    1.59  val isolate_bdvs_4x4 = 
    1.60      Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [], 
    1.61 -	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
    1.62 +	 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.63  	 erls = Rule_Set.append_rules 
    1.64  		    "erls_isolate_bdvs_4x4" Rule_Set.empty 
    1.65  		    [Rule.Num_Calc ("EqSystem.occur'_exactly'_in", 
    1.66 @@ -339,9 +339,9 @@
    1.67  
    1.68  val prls_triangular = 
    1.69      Rule_Def.Repeat {id="prls_triangular", preconds = [], 
    1.70 -	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
    1.71 +	 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.72  	 erls = Rule_Def.Repeat {id="erls_prls_triangular", preconds = [], 
    1.73 -		     rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
    1.74 +		     rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.75  		     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.76  		     rules = [(*for precond NTH_CONS ...*)
    1.77  			      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.78 @@ -368,9 +368,9 @@
    1.79   more similarity to prls_triangular desirable*)
    1.80  val prls_triangular4 = 
    1.81      Rule_Def.Repeat {id="prls_triangular4", preconds = [], 
    1.82 -	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
    1.83 +	 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.84  	 erls = Rule_Def.Repeat {id="erls_prls_triangular4", preconds = [], 
    1.85 -		     rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
    1.86 +		     rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.87  		     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.88  		     rules = [(*for precond NTH_CONS ...*)
    1.89  			      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),