1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4  
     1.5  val ordne_alphabetisch = 
     1.6    Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], 
     1.7 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.8 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.9      erls = erls_ordne_alphabetisch, 
    1.10      rules = [
    1.11        \<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*)
    1.12 @@ -206,7 +206,7 @@
    1.13  
    1.14  val fasse_zusammen = 
    1.15    Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 
    1.16 -	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.17 +	  rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
    1.18  	  erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 
    1.19  	  	[\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")],
    1.20  	  srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.21 @@ -248,7 +248,7 @@
    1.22      
    1.23  val verschoenere = 
    1.24    Rule_Def.Repeat{id = "verschoenere", preconds = [], 
    1.25 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.26 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.27      erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty 
    1.28  		  [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
    1.29      rules = [
    1.30 @@ -268,7 +268,7 @@
    1.31  
    1.32  val klammern_aufloesen = 
    1.33    Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], 
    1.34 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, 
    1.35 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, 
    1.36      calc = [], errpatts = [], erls = Rule_Set.Empty, 
    1.37      rules = [
    1.38        \<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*)
    1.39 @@ -279,7 +279,7 @@
    1.40  
    1.41  val klammern_ausmultiplizieren = 
    1.42    Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], 
    1.43 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, 
    1.44 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, 
    1.45      calc = [], errpatts = [], erls = Rule_Set.Empty, 
    1.46      rules = [
    1.47        \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
    1.48 @@ -291,7 +291,7 @@
    1.49  
    1.50  val ordne_monome = 
    1.51    Rule_Def.Repeat {
    1.52 -    id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
    1.53 +    id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
    1.54      srls = Rule_Set.Empty, calc = [], errpatts = [], 
    1.55      erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [
    1.56        \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),