1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4    #2 NOT using common_nominator_p                          .*)
     1.5  val norm_System_noadd_fractions = 
     1.6    Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [], 
     1.7 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
     1.8 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     1.9      erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.10      rules = [(*sequence given by operator precedence*)
    1.11    		Rule.Rls_ discard_minus,
    1.12 @@ -209,7 +209,7 @@
    1.13    *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
    1.14  val norm_System = 
    1.15    Rule_Def.Repeat {id = "norm_System", preconds = [], 
    1.16 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
    1.17 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
    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 @@ -235,7 +235,7 @@
    1.22     analoguous to simplify_Integral                                       .*)
    1.23  val simplify_System_parenthesized = 
    1.24    Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list, 
    1.25 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.26 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
    1.27      erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.28      rules = [
    1.29         \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
    1.30 @@ -255,7 +255,7 @@
    1.31  (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
    1.32  val simplify_System = 
    1.33    Rule_Set.Sequence {id = "simplify_System", preconds = []:term list, 
    1.34 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.35 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
    1.36      erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.37      rules = [
    1.38        Rule.Rls_ norm_Rational,
    1.39 @@ -274,7 +274,7 @@
    1.40  ML \<open>
    1.41  val isolate_bdvs = 
    1.42    Rule_Def.Repeat {
    1.43 -    id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.44 +    id="isolate_bdvs", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
    1.45      erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [
    1.46        (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))], 
    1.47      srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.48 @@ -287,7 +287,7 @@
    1.49  ML \<open>
    1.50  val isolate_bdvs_4x4 = 
    1.51    Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [], 
    1.52 -    rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.53 +    rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
    1.54      erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [
    1.55        \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
    1.56        \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    1.57 @@ -318,9 +318,9 @@
    1.58  
    1.59  val prls_triangular = 
    1.60    Rule_Def.Repeat {
    1.61 -    id="prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.62 +    id="prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
    1.63      erls = Rule_Def.Repeat {
    1.64 -      id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.65 +      id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
    1.66        erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.67        rules = [(*for precond NTH_CONS ...*)
    1.68           \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.69 @@ -344,9 +344,9 @@
    1.70   more similarity to prls_triangular desirable*)
    1.71  val prls_triangular4 = 
    1.72    Rule_Def.Repeat {
    1.73 -  id="prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.74 +  id="prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
    1.75    erls = Rule_Def.Repeat {
    1.76 -    id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.77 +    id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
    1.78      erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.79      rules = [(*for precond NTH_CONS ...*)
    1.80    	   \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),