1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Apr 08 16:56:47 2020 +0200
     1.3 @@ -192,7 +192,7 @@
     1.4  
     1.5  val ordne_alphabetisch = 
     1.6    Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], 
     1.7 -      rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.8 +      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.9        erls = erls_ordne_alphabetisch, 
    1.10        rules = [Rule.Thm ("tausche_plus",TermC.num_str @{thm tausche_plus}),
    1.11  	       (*"b kleiner a ==> (b + a) = (a + b)"*)
    1.12 @@ -214,7 +214,7 @@
    1.13  
    1.14  val fasse_zusammen = 
    1.15      Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 
    1.16 -	rew_ord = ("dummy_ord", Rule.dummy_ord),
    1.17 +	rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.18  	erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 
    1.19  			  [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")], 
    1.20  	srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.21 @@ -280,7 +280,7 @@
    1.22      
    1.23  val verschoenere = 
    1.24    Rule_Def.Repeat{id = "verschoenere", preconds = [], 
    1.25 -      rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.26 +      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.27        erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty 
    1.28  			[Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner "")], 
    1.29        rules = [Rule.Thm ("vorzeichen_minus_weg1",TermC.num_str @{thm vorzeichen_minus_weg1}),
    1.30 @@ -311,7 +311,7 @@
    1.31  
    1.32  val klammern_aufloesen = 
    1.33    Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], 
    1.34 -      rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 
    1.35 +      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 
    1.36        rules = [Rule.Thm ("sym_add_assoc",
    1.37                       TermC.num_str (@{thm add.assoc} RS @{thm sym})),
    1.38  	       (*"a + (b + c) = (a + b) + c"*)
    1.39 @@ -325,7 +325,7 @@
    1.40  
    1.41  val klammern_ausmultiplizieren = 
    1.42    Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], 
    1.43 -      rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 
    1.44 +      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 
    1.45        rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
    1.46  	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
    1.47  	       Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
    1.48 @@ -342,7 +342,7 @@
    1.49  
    1.50  val ordne_monome = 
    1.51    Rule_Def.Repeat{id = "ordne_monome", preconds = [], 
    1.52 -      rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], 
    1.53 +      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], 
    1.54        erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty
    1.55  	       [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner ""),
    1.56  		Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "")