# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1285246163 -7200
# Node ID 3e11e3c2dc42c5f5ef0401350f2290ed14745ff7
# Parent  e4f42a63d6656af68505f77d546adf2c01b8206c
updated "op +", "op -", "op *". "HOL.divide" in src & test

find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;

diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Interpret/solve.sml
--- a/src/Tools/isac/Interpret/solve.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Interpret/solve.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -91,7 +91,7 @@
 
 (*13.9.02--------------
 type ctr = (loc * pos) list;
-val ops = [("PLUS","op +"),("MINUS","op -"),("TIMES","op *"),
+val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","op *"),
 	   ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
 ML {* 
 @{term "PLUS"};   (*Free ("PLUS", "'a") : term*)
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Atools.thy
--- a/src/Tools/isac/Knowledge/Atools.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Atools.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -240,7 +240,7 @@
   | eval_const _ _ _ _ = NONE; 
 
 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
-(*("PLUS"    ,("op +"        ,eval_binop "#add_")),
+(*("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
   ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
   ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)
 
@@ -278,8 +278,8 @@
 	case (numeral t1, numeral t2) of
 	    (SOME n1, SOME n2) =>
 	    let val (T1,T2,Trange) = dest_binop_typ t0
-		val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
-		(*WN071229 "HOL.divide" never tried*)
+		val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
+		(*WN071229 "Rings.inverse_class.divide" never tried*)
 		val rhs = var_op_float v op_ t0 T1 res
 		val prop = Trueprop $ (mk_equality (t, rhs))
 	    in SOME (mk_thmid_f thmid n1 n2, prop) end
@@ -293,7 +293,7 @@
   if op0 = op0' then
 	case (numeral t1, numeral t2) of
 	    (SOME n1, SOME n2) =>
-	    if op0 = "op -" then NONE else
+	    if op0 = "Groups.minus_class.minus" then NONE else
 	    let val (T1,T2,Trange) = dest_binop_typ t0
 		val res = calc op0 n1 n2
 		val rhs = float_op_var v op_ t0 T1 res
@@ -314,7 +314,7 @@
        | _ => NONE)
   | eval_binop _ _ _ _ = NONE; 
 (*
-> val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
+> val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
 > term2str t;
 val it = "-1 + 2 = 1"
 > val t = str2term "-1 * (-1 * a)";
@@ -449,8 +449,8 @@
 (** evaluation on the metalevel **)
 
 (*. evaluate HOL.divide .*)
-(*("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e"))*)
-fun eval_cancel (thmid:string) "HOL.divide" (t as 
+(*("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"))*)
+fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as 
 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
     (case (int_of_str n1, int_of_str n2) of
 	 (SOME n1', SOME n2') =>
@@ -523,10 +523,10 @@
   | list2sum [s] = s
   | list2sum (s::ss) = 
     let fun sum su [s'] = 
-	    Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
+	    Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		  $ su $ s'
 	  | sum su (s'::ss') = 
-	    sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
+	    sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		  $ su $ s') ss'
     in sum s ss end;
 
@@ -561,7 +561,7 @@
 val list_rls = 
     append_rls "list_rls" list_rls
 	       [Calc ("op *",eval_binop "#mult_"),
-		Calc ("op +", eval_binop "#add_"), 
+		Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 		Calc ("op <",eval_equ "#less_"),
 		Calc ("op <=",eval_equ "#less_equal_"),
 		Calc ("Atools.ident",eval_ident "#ident_"),
@@ -591,8 +591,8 @@
 		Calc ("op =",eval_equal "#equal_"),
 
 		Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
-		Calc ("op +",eval_binop "#add_"),
-		Calc ("op -",eval_binop "#sub_"),
+		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
 		Calc ("op *",eval_binop "#mult_")
 		];
 
@@ -708,10 +708,10 @@
     ("leq"      ,("op <="       ,eval_equ "#less_equal_")),
     ("ident"    ,("Atools.ident",eval_ident "#ident_")),
     ("equal"    ,("op =",eval_equal "#equal_")),
-    ("PLUS"     ,("op +"        ,eval_binop "#add_")),
-    ("MINUS"    ,("op -",eval_binop "#sub_")),
+    ("PLUS"     ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
+    ("MINUS"    ,("Groups.minus_class.minus",eval_binop "#sub_")),
     ("TIMES"    ,("op *"        ,eval_binop "#mult_")),
-    ("DIVIDE"  ,("HOL.divide"  ,eval_cancel "#divide_e")),
+    ("DIVIDE"  ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
     ("POWER"   ,("Atools.pow"  ,eval_binop "#power_")),
     ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
     ]);
@@ -724,7 +724,7 @@
 				rew_ord = ("termlessI",termlessI), 
 				erls = e_rls, 
 				srls = Erls, calc = [], (*asm_thm = [],*)
-				rules = [Calc ("op +", eval_binop "#add_"),
+				rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 					 Calc ("op <",eval_equ "#less_")
 					 (*    ~~~~~~ for nth_Cons_*)
 					 ],
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Biegelinie.thy
--- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -185,11 +185,11 @@
 				  [(*for asm in NTH_CONS ...*)
 				   Calc ("op <",eval_equ "#less_"),
 				   (*2nd NTH_CONS pushes n+-1 into asms*)
-				   Calc("op +", eval_binop "#add_")
+				   Calc("Groups.plus_class.plus", eval_binop "#add_")
 				   ], 
 		srls = Erls, calc = [],
 		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
-			 Calc("op +", eval_binop "#add_"),
+			 Calc("Groups.plus_class.plus", eval_binop "#add_"),
 			 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
 			 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
 			 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
@@ -206,11 +206,11 @@
 			   [(*for asm in NTH_CONS ...*)
 			    Calc ("op <",eval_equ "#less_"),
 			    (*2nd NTH_CONS pushes n+-1 into asms*)
-			    Calc("op +", eval_binop "#add_")
+			    Calc("Groups.plus_class.plus", eval_binop "#add_")
 			    ], 
 	 srls = Erls, calc = [],
 	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
-		  Calc("op +", eval_binop "#add_"),
+		  Calc("Groups.plus_class.plus", eval_binop "#add_"),
 		  Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
 		  Calc("Tools.lhs", eval_lhs "eval_lhs_"),
 		  Calc("Atools.filter'_sameFunId",
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Delete.thy
--- a/src/Tools/isac/Knowledge/Delete.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Delete.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -19,15 +19,15 @@
 
 (*.used for calculating built in binary operations in Isabelle2002.
    integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
-fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int)  = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
+fun calc "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int)  = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
     if b < d 
     then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
     else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
-  | calc "op -" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
+  | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
     ((a - c,0),(0,0))
   | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
     ((a * c, b + d), (0, 0))
-  | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
+  | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
     ((a div c, 0), (0, 0))
   | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
     ((power a c, 0), (0, 0))
@@ -37,7 +37,7 @@
 		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
 		 (string_of_int c  )^","^(string_of_int d  )^"), ("^
 		 (string_of_int p21)^","^(string_of_int p22)^"))");
-(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); 
+(*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); 
 val it = ((1,0),(0,0))*)
 
 (*.convert internal floatingpoint prepresentation to int and float.*)
@@ -76,9 +76,9 @@
 				    (Free (str_of_int p2, T)))))
     end;
 (*> val t = str2term "a + b";
-> val Const ("op +", optype) $ _ $ _ = t;
+> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
-> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
+> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
 val it = true : bool*)
 
 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
@@ -94,9 +94,9 @@
 				    (Free (str_of_int p2, T))))) $ v
     end;
 (*> val t = str2term "a + b";
-> val Const ("op +", optype) $ _ $ _ = t;
+> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
-> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
+> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
 val it = true : bool*)
 *}
 
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -274,7 +274,7 @@
 	       (*Rls_ discard_parentheses *3**),
 	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
 	       Rls_ separate_bdv2,
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 	       ],
       scr = EmptyScr}:rls;      
 *}
@@ -292,7 +292,7 @@
 	       Rls_ discard_parentheses,
 	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
 	       Rls_ separate_bdv2,
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 	       ],
       scr = EmptyScr}:rls;      
 (*
@@ -362,14 +362,14 @@
 		     erls = Erls, srls = Erls, calc = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Calc ("op <",eval_equ "#less_"),
-			      Calc ("op +", eval_binop "#add_")
+			      Calc ("Groups.plus_class.plus", eval_binop "#add_")
 			      (*immediately repeated rewrite pushes
 					    '+' into precondition !*)
 			      ],
 		     scr = EmptyScr}, 
 	 srls = Erls, calc = [],
 	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
-		  Calc ("op +", eval_binop "#add_"),
+		  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
 		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
 		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
@@ -391,14 +391,14 @@
 		     erls = Erls, srls = Erls, calc = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Calc ("op <",eval_equ "#less_"),
-			      Calc ("op +", eval_binop "#add_")
+			      Calc ("Groups.plus_class.plus", eval_binop "#add_")
 			      (*immediately repeated rewrite pushes
 					    '+' into precondition !*)
 			      ],
 		     scr = EmptyScr}, 
 	 srls = Erls, calc = [],
 	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
-		  Calc ("op +", eval_binop "#add_"),
+		  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
 		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
 		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
@@ -458,7 +458,7 @@
   append_rls "prls_2x2_linear_system" e_rls 
 			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
 			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
-			      Calc ("op +", eval_binop "#add_"),
+			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 			      Calc ("op =",eval_equal "#equal_")
 			      ], 
   SOME "solveSystem e_s v_s", 
@@ -497,7 +497,7 @@
   append_rls "prls_3x3_linear_system" e_rls 
 			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
 			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
-			      Calc ("op +", eval_binop "#add_"),
+			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 			      Calc ("op =",eval_equal "#equal_")
 			      ], 
   SOME "solveSystem e_s v_s", 
@@ -513,7 +513,7 @@
   append_rls "prls_4x4_linear_system" e_rls 
 			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
 			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
-			      Calc ("op +", eval_binop "#add_"),
+			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 			      Calc ("op =",eval_equal "#equal_")
 			      ], 
   SOME "solveSystem e_s v_s", 
@@ -672,11 +672,11 @@
 				  [(*for asm in NTH_CONS ...*)
 				   Calc ("op <",eval_equ "#less_"),
 				   (*2nd NTH_CONS pushes n+-1 into asms*)
-				   Calc("op +", eval_binop "#add_")
+				   Calc("Groups.plus_class.plus", eval_binop "#add_")
 				   ], 
 		srls = Erls, calc = [],
 		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
-			 Calc("op +", eval_binop "#add_"),
+			 Calc("Groups.plus_class.plus", eval_binop "#add_"),
 			 Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
 		scr = EmptyScr};
 store_met
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -140,7 +140,7 @@
 		  Thm ("integral_add",num_str @{thm integral_add}),
 		  Thm ("integral_mult",num_str @{thm integral_mult}),
 		  Thm ("integral_pow",num_str @{thm integral_pow}),
-		  Calc ("op +", eval_binop "#add_")(*for n+1*)
+		  Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
 		  ],
 	 scr = EmptyScr};
 *}
@@ -200,7 +200,7 @@
 	       Thm ("divide_divide_eq_left",
                      num_str @{thm divide_divide_eq_left}),
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
 	      
 	       Thm ("rat_power", num_str @{thm rat_power})
 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
@@ -264,7 +264,7 @@
 	       Rls_ discard_parentheses,
 	       (*Rls_ collect_bdv, from make_polynomial_in*)
 	       Rls_ separate_bdv2,
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 	       ],
       scr = EmptyScr}:rls;      
 
@@ -302,7 +302,7 @@
 * 				 num_str @{thm add_divide_distrib})
 * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
 * 			  ]),
-* 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+* 	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 * 	       ],
 *       scr = EmptyScr
 *       }:rls); 
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -55,7 +55,7 @@
    [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Calc ("HOL.divide", eval_cancel "#divide_e"),
+     Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
      Calc ("Atools.pow" ,eval_binop "#power_"),
      *)
     ];
@@ -66,7 +66,7 @@
    [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Calc ("HOL.divide", eval_cancel "#divide_e"),
+     Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
      Calc ("Atools.pow" ,eval_binop "#power_"),
      *)
     ];
@@ -84,11 +84,11 @@
        (*asm_thm = [],*)
        rules = [
 		Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),
-		Calc ("op +",eval_binop "#add_"),
-		Calc ("op -",eval_binop "#sub_"),
+		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
 		Calc ("op *",eval_binop "#mult_"),
 		(*  Dont use  
-		 Calc ("HOL.divide", eval_cancel "#divide_e"),		
+		 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),		
 		 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 		 *)
 		Calc ("Atools.pow" ,eval_binop "#power_")
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -177,7 +177,7 @@
     let fun coeff_in c v = member op = (vars c) v;
    	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
 	    (* at the moment there is no term like this, but ....*)
-	  | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = 
+	  | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = 
             not(coeff_in b v)
 	  | finddivide (_ $ t1 $ t2) v = 
             (finddivide t1 v) orelse (finddivide t2 v)
@@ -250,21 +250,21 @@
      (*val it = NONE*)
     ------------------------------------------------------------------*)
     fun expand_deg_in t v =
-    	let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
+    	let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
     		(case mono_deg_in t2 v of (* $ is left associative*)
     		     SOME d' => edi d' d' t1
 		   | NONE => NONE)
-    	      | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
+    	      | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
     		(case mono_deg_in t2 v of
     		     SOME d' => edi d' d' t1
 		   | NONE => NONE)
-    	      | edi d dmax (Const ("op -",_) $ t1 $ t2) =
+    	      | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
     		(case mono_deg_in t2 v of
 		(*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
     		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
                      then edi d' dmax t1 else NONE
 		   | NONE => NONE)
-    	      | edi d dmax (Const ("op +",_) $ t1 $ t2) =
+    	      | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
     		(case mono_deg_in t2 v of
 		(*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
     		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
@@ -297,11 +297,11 @@
      expand_deg_in t v;
     -------------------------------------------------------------------*)   
     fun poly_deg_in t v =
-    	let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
+    	let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
     		(case mono_deg_in t2 v of (* $ is left associative*)
     		     SOME d' => edi d' d' t1
 		   | NONE => NONE)
-    	      | edi d dmax (Const ("op +",_) $ t1 $ t2) =
+    	      | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
     		(case mono_deg_in t2 v of
  		(*RL  orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
    		     SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) 
@@ -399,8 +399,8 @@
     append_rls "Poly_erls" Atools_erls
                [ Calc ("op =",eval_equal "#equal_"),
 		 Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
-                 Calc ("op +",eval_binop "#add_"),
-		 Calc ("op -",eval_binop "#sub_"),
+                 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
 		 Calc ("op *",eval_binop "#mult_"),
 		 Calc ("Atools.pow" ,eval_binop "#power_")
 		 ];
@@ -409,8 +409,8 @@
     append_rls "poly_crls" Atools_crls
                [ Calc ("op =",eval_equal "#equal_"),
 		 Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
-                 Calc ("op +",eval_binop "#add_"),
-		 Calc ("op -",eval_binop "#sub_"),
+                 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
 		 Calc ("op *",eval_binop "#mult_"),
 		 Calc ("Atools.pow" ,eval_binop "#power_")
 		 ];
@@ -553,13 +553,13 @@
 (*.the expression contains + - * ^ only ?
    this is weaker than 'is_polynomial' !.*)
 fun is_polyexp (Free _) = true
-  | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true
-  | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true
+  | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
+  | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
   | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
   | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
-  | is_polyexp (Const ("op +",_) $ t1 $ t2) = 
+  | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
                ((is_polyexp t1) andalso (is_polyexp t2))
-  | is_polyexp (Const ("op -",_) $ t1 $ t2) = 
+  | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = 
                ((is_polyexp t1) andalso (is_polyexp t2))
   | is_polyexp (Const ("op *",_) $ t1 $ t2) = 
                ((is_polyexp t1) andalso (is_polyexp t2))
@@ -658,12 +658,12 @@
   Rls{id = "calc_add_mult_pow_", preconds = [], 
       rew_ord = ("dummy_ord", dummy_ord),
       erls = Atools_erls(*erls3.4.03*),srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
       (*asm_thm = [],*)
-      rules = [Calc ("op +", eval_binop "#add_"),
+      rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 	       Calc ("op *", eval_binop "#mult_"),
 	       Calc ("Atools.pow", eval_binop "#power_")
 	       ], scr = EmptyScr}:rls;
@@ -689,7 +689,7 @@
   Rls{id = "collect_numerals_", preconds = [], 
       rew_ord = ("dummy_ord", dummy_ord),
       erls = Atools_erls, srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_"))
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_"))
 	      ],
       rules = 
         [Thm ("real_num_collect",num_str @{thm real_num_collect}), 
@@ -702,7 +702,7 @@
 	 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}), 
 	     (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
 
-         Calc ("op +", eval_binop "#add_"),
+         Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 
 	 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
 		     (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
@@ -751,7 +751,7 @@
   Rls{id = "collect_numerals", preconds = [], 
       rew_ord = ("dummy_ord", dummy_ord),
       erls = Atools_erls(*erls3.4.03*),srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
@@ -766,7 +766,7 @@
 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
 	       (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
 	       
-	       Calc ("op +", eval_binop "#add_"),
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 
 	       (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
 	       Thm ("sym_real_mult_2",
@@ -879,7 +879,7 @@
   Rls{id = "collect_numerals", preconds = [], 
       rew_ord = ("dummy_ord", dummy_ord),
       erls = Atools_erls(*erls3.4.03*),srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
@@ -893,7 +893,7 @@
 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
-	       Calc ("op +", eval_binop "#add_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	       Calc ("op *", eval_binop "#mult_"),
 	       Calc ("Atools.pow", eval_binop "#power_")
 	       ], scr = EmptyScr}:rls;
@@ -1024,7 +1024,7 @@
 val expand_binoms = 
   Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
       erls = Atools_erls, srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
@@ -1079,7 +1079,7 @@
                (*"0 * z = 0"*)
 	       Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	       Calc ("op *", eval_binop "#mult_"),
 	       Calc ("Atools.pow", eval_binop "#power_"),
               (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
@@ -1114,7 +1114,7 @@
                      num_str @{thm real_one_collect_assoc}), 
 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	       Calc ("op *", eval_binop "#mult_"),
 	       Calc ("Atools.pow", eval_binop "#power_")
 	       ],
@@ -1127,7 +1127,7 @@
 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
 (* Polynom --> List von Monomen *) 
-fun poly2list (Const ("op +",_) $ t1 $ t2) = 
+fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
     (poly2list t1) @ (poly2list t2)
   | poly2list t = [t];
 
@@ -1277,7 +1277,7 @@
 
 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt 
    (mit gewuenschtem Typen T) *)
-fun plus T = Const ("op +", [T,T] ---> T);
+fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
 fun mult T = Const ("op *", [T,T] ---> T);
 fun binop op_ t1 t2 = op_ $ t1 $ t2;
 fun create_prod T (a,b) = binop (mult T) a b;
@@ -1352,9 +1352,9 @@
 	  erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
 			    [Calc ("Poly.is'_multUnordered", 
                                     eval_is_multUnordered "")],
-	  calc = [("PLUS"  , ("op +"      , eval_binop "#add_")),
+	  calc = [("PLUS"  , ("Groups.plus_class.plus"      , eval_binop "#add_")),
 		  ("TIMES" , ("op *"      , eval_binop "#mult_")),
-		  ("DIVIDE", ("HOL.divide", eval_cancel "#divide_e")),
+		  ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
 		  ("POWER" , ("Atools.pow", eval_binop "#power_"))],
 	  scr=Rfuns {init_state  = init_state,
 		     normal_form = normal_form,
@@ -1405,9 +1405,9 @@
 			    [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
 			     (*WN.18.6.03 definiert in thy,
                                evaluiert prepat*)],
-	  calc = [("PLUS"    ,("op +"        ,eval_binop "#add_")),
+	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
-		  ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
+		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  (*asm_thm=[],*)
 	  scr=Rfuns {init_state  = init_state,
@@ -1491,7 +1491,7 @@
 val rev_rew_p = 
 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
     erls = Atools_erls, srls = Erls,
-    calc = [(*("PLUS"  , ("op +", eval_binop "#add_")), 
+    calc = [(*("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	    ("TIMES" , ("op *", eval_binop "#mult_")),
 	    ("POWER", ("Atools.pow", eval_binop "#power_"))*)
 	    ],
@@ -1514,7 +1514,7 @@
 	     Rls_ order_mult_rls_,
 	     (*Rls_ order_add_rls_,*)
 
-	     Calc ("op +", eval_binop "#add_"), 
+	     Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	     Calc ("op *", eval_binop "#mult_"),
 	     Calc ("Atools.pow", eval_binop "#power_"),
 	     
@@ -1540,7 +1540,7 @@
 	     Thm ("realpow_multI", num_str @{thm realpow_multI}),
 	     (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
 
-	     Calc ("op +", eval_binop "#add_"), 
+	     Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	     Calc ("op *", eval_binop "#mult_"),
 	     Calc ("Atools.pow", eval_binop "#power_"),
 
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -457,10 +457,10 @@
 		Thm  ("real_diff_minus",num_str @{thm real_diff_minus}),
 		Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
 		Thm  ("realpow_multI",num_str @{thm realpow_multI}),
-		Calc ("op +",eval_binop "#add_"),
-		Calc ("op -",eval_binop "#sub_"),
+		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
 		Calc ("op *",eval_binop "#mult_"),
-		Calc ("HOL.divide", eval_cancel "#divide_e"),
+		Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
 		Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 		Calc ("Atools.pow" ,eval_binop "#power_"),
                 Rls_ reduce_012
@@ -1481,7 +1481,7 @@
 	       Rls_ separate_bdvs,
 	       (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
 	       Rls_ cancel_p
-	       (*Calc ("HOL.divide"  ,eval_cancel "#divide_e") too weak!*)
+	       (*Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e") too weak!*)
 	       ],
       scr = EmptyScr}:rls);      
 
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/PolyMinus.thy
--- a/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -262,8 +262,8 @@
 	 Thm ("subtrahiere_x_minus_minus1",num_str @{thm subtrahiere_x_minus_minus1}),
 	 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
 	 
-	 Calc ("op +", eval_binop "#add_"),
-	 Calc ("op -", eval_binop "#subtr_"),
+	 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
+	 Calc ("Groups.minus_class.minus", eval_binop "#subtr_"),
 	 
 	 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
            (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
@@ -382,8 +382,8 @@
 val rechnen = 
     append_rls "rechnen" e_rls
 	       [Calc ("op *", eval_binop "#mult_"),
-		Calc ("op +", eval_binop "#add_"),
-		Calc ("op -", eval_binop "#subtr_")
+		Calc ("Groups.plus_class.plus", eval_binop "#add_"),
+		Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
 		];
 
 ruleset' := 
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/RatEq.thy
--- a/src/Tools/isac/Knowledge/RatEq.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/RatEq.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -52,7 +52,7 @@
 	fun coeff_in c v = member op = (vars c) v;
    	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
 	    (* at the moment there is no term like this, but ....*)
-	  | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
+	  | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
 	  | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) 
                                          orelse (finddivide t2 v)
 	  | finddivide (_ $ t1) v = (finddivide t1 v)
@@ -94,7 +94,7 @@
 	(merge_rls "is_ratequation_in" calculate_Rational
 		   (append_rls "is_ratequation_in"
 			Poly_erls
-			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)
+			[(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
 			 Calc ("RatEq.is'_ratequation'_in",
 			       eval_is_ratequation_in "")
 
@@ -112,7 +112,7 @@
 	(merge_rls "is_ratequation_in" calculate_Rational
 		   (append_rls "is_ratequation_in"
 			Poly_erls
-			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)
+			[(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
 			 Calc ("RatEq.is'_ratequation'_in",
 			       eval_is_ratequation_in "")
 			 ]))
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Rational-WN.sml
--- a/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -63,7 +63,7 @@
     else raise error ("term2poly.2 "^term2str t)
   | mono t _ _ = raise error ("term2poly.3 "^term2str t);
 
-fun poly (Const ("op +",_) $ t1 $ t2) v g = 
+fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = 
     let val l = mono t1 v g
     in (l @ (poly t2 v ((length l) + g))) end
   | poly t v g = mono t v g;
@@ -73,7 +73,7 @@
 				  handle _ => NONE)
   | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
     if t = v then SOME [0, (the o int_of_str) s1] else NONE
-  | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v = 
+  | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = 
     SOME ([(the o int_of_str) s1] @ (poly t v 1))
   | term2poly t v = 
     SOME (poly t v 0) handle _ => NONE;
@@ -144,7 +144,7 @@
 (cterm_of thy) t;
 
 
-fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;
+fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
 
 
 fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -1324,7 +1324,7 @@
   | test_polynomial (t as Free(str,_)) v = true
   | test_polynomial (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
 						     else (test_polynomial t1 "*") andalso (test_polynomial t2 "*")
-  | test_polynomial (t as Const ("op +",_) $ t1 $ t2) v = if v="*" orelse v="^" then false 
+  | test_polynomial (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false 
 							  else (test_polynomial t1 " ") andalso (test_polynomial t2 " ")
   | test_polynomial (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_polynomial t1 "^") andalso (test_polynomial t2 "^")
   | test_polynomial _ v = false;  
@@ -1337,9 +1337,9 @@
 fun test_exp (t as Free(str,_)) v = true 
   | test_exp (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
 						     else (test_exp t1 "*") andalso (test_exp t2 "*")
-  | test_exp (t as Const ("op +",_) $ t1 $ t2) v = if v="*" orelse v="^" then false 
+  | test_exp (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false 
 							  else (test_exp t1 " ") andalso (test_exp t2 " ") 
-  | test_exp (t as Const ("op -",_) $ t1 $ t2) v = if v="*" orelse v="^" then false 
+  | test_exp (t as Const ("Groups.minus_class.minus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false 
 							  else (test_exp t1 " ") andalso (test_exp t2 " ")
   | test_exp (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_exp t1 "^") andalso (test_exp t2 "^")
   | test_exp  _ v = false;
@@ -1429,11 +1429,11 @@
      else raise error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
 	 )
     end
-  | term2coef' (Const ("op +",_) $ t1 $ t2) v :mv_poly option= 
+  | term2coef' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option= 
     (
      SOME ((the(term2coef' t1 v)) @ (the(term2coef' t2 v))) handle _ => NONE
 	 )
-  | term2coef' (Const ("op -",_) $ t1 $ t2) v :mv_poly option= 
+  | term2coef' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option= 
     (
      SOME ((the(term2coef' t1 v)) @ mv_skalar_mul((the(term2coef' t2 v)),1)) handle _ => NONE
 	 )
@@ -1544,11 +1544,11 @@
      else raise error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
 	 )
     end
-  | term2poly' (Const ("op +",_) $ t1 $ t2) v :mv_poly option = 
+  | term2poly' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option = 
     (
      SOME ((the(term2poly' t1 v)) @ (the(term2poly' t2 v))) handle _ => NONE
 	 )
-  | term2poly' (Const ("op -",_) $ t1 $ t2) v :mv_poly option = 
+  | term2poly' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option = 
     (
      SOME ((the(term2poly' t1 v)) @ mv_skalar_mul((the(term2poly' t2 v)),~1)) handle _ => NONE
 	 )
@@ -1674,7 +1674,7 @@
 fun poly2term' ([] : mv_poly, vs) = Free(str_of_int 0, HOLogic.realT)  
   | poly2term' ([(c, e) : mv_monom], vs) = monom2term ((c, e), vs)
   | poly2term' ((c, e) :: ces, vs) =  
-    Const("op +", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
+    Const("Groups.plus_class.plus", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
          poly2term (ces, vs) $ monom2term ((c, e), vs)
 and poly2term (xs, vs) = poly2term' (rev (sort (mv_geq LEX_) (xs)), vs);
 
@@ -1709,13 +1709,13 @@
   | exp2term' ([(c,e)],vars) =     monom2term((c,e),vars) 			     
   | exp2term' ((c1,e1)::others,vars) =  
     if c1<0 then 	
-	Const("op -",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+	Const("Groups.minus_class.minus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 	exp2term'(others,vars) $
 	( 
 	 monom2term2((c1,e1),vars)
 	 ) 
     else
-	Const("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
+	Const("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
 	exp2term'(others,vars) $
 	( 
 	 monom2term2((c1,e1),vars)
@@ -1743,7 +1743,7 @@
 
 
 (*. calculates the greatest common divisor of numerator and denominator and seperates it from each .*)
-fun step_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) = 
+fun step_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) = 
     let
 	val p1' = Unsynchronized.ref [];
 	val p2' = Unsynchronized.ref [];
@@ -1756,7 +1756,7 @@
 	 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));
 	 if (!p3)=[(1,mv_null2(vars))] then 
 	     (
-	      Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
+	      Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
 	      )
 	 else
 	     (
@@ -1766,7 +1766,7 @@
 	      
 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
 	      (
-	       Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+	       Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 	       $ 
 	       (
 		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -1786,7 +1786,7 @@
 	       p2':=mv_skalar_mul(!p2',~1);
 	       p3:=mv_skalar_mul(!p3,~1);
 	       (
-		Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		$ 
 		(
 		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -1808,7 +1808,7 @@
 
 
 (*. same as step_cancel, this time for expanded forms (input+output) .*)
-fun step_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) = 
+fun step_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) = 
     let
 	val p1' = Unsynchronized.ref [];
 	val p2' = Unsynchronized.ref [];
@@ -1821,7 +1821,7 @@
 	 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));
 	 if (!p3)=[(1,mv_null2(vars))] then 
 	     (
-	      Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
+	      Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
 	      )
 	 else
 	     (
@@ -1831,7 +1831,7 @@
 	      
 	      if #1(hd(sort (mv_geq LEX_) (!p2')))(* mv_lc2(!p2',LEX_)*)>0 then
 	      (
-	       Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+	       Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 	       $ 
 	       (
 		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -1851,7 +1851,7 @@
 	       p2':=mv_skalar_mul(!p2',~1);
 	       p3:=mv_skalar_mul(!p3,~1);
 	       (
-		Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		$ 
 		(
 		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -1872,7 +1872,7 @@
 | step_cancel_expanded _ = raise error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction"); 
 
 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
-fun direct_cancel (t as Const ("HOL.divide",_) $ p1 $ p2) = 
+fun direct_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) = 
     let
 	val p1' = Unsynchronized.ref [];
 	val p2' = Unsynchronized.ref [];
@@ -1886,7 +1886,7 @@
 
 	 if (!p3)=[(1,mv_null2(vars))] then 
 	     (
-	      (Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
+	      (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
 	      )
 	 else
 	     (
@@ -1895,7 +1895,7 @@
 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then	      
 	      (
 	       (
-		Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		$ 
 		(
 		 poly2term((!p1'),vars)
@@ -1926,7 +1926,7 @@
 		   p2':=mv_skalar_mul(!p2',~1);
 		   if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1); 
 		       (
-			Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+			Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 			$ 
 			(
 			 poly2term((!p1'),vars)
@@ -1957,7 +1957,7 @@
   | direct_cancel _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction"); 
 
 (*. same es direct_cancel, this time for expanded forms (input+output).*) 
-fun direct_cancel_expanded (t as Const ("HOL.divide",_) $ p1 $ p2) =  
+fun direct_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =  
     let
 	val p1' = Unsynchronized.ref [];
 	val p2' = Unsynchronized.ref [];
@@ -1971,7 +1971,7 @@
 
 	 if (!p3)=[(1,mv_null2(vars))] then 
 	     (
-	      (Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
+	      (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
 	      )
 	 else
 	     (
@@ -1980,7 +1980,7 @@
 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then	      
 	      (
 	       (
-		Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		$ 
 		(
 		 poly2expanded((!p1'),vars)
@@ -2011,7 +2011,7 @@
 		   p2':=mv_skalar_mul(!p2',~1);
 		   if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1); 
 		       (
-			Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+			Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 			$ 
 			(
 			 poly2expanded((!p1'),vars)
@@ -2043,7 +2043,7 @@
 
 
 (*. adds two fractions .*)
-fun add_fract ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
+fun add_fract ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
     let
 	val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
 	val t11'= Unsynchronized.ref  (the(term2poly t11 vars));
@@ -2074,7 +2074,7 @@
 				LEX_));
 writeln"### add_fract: done sort mv_add";
 	 (
-	  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+	  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 	  $ 
 	  (
 	   poly2term((!nom),vars)
@@ -2089,7 +2089,7 @@
   | add_fract (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
 
 (*. adds two expanded fractions .*)
-fun add_fract_exp ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
+fun add_fract_exp ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
     let
 	val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
 	val t11'= Unsynchronized.ref  (the(expanded2poly t11 vars));
@@ -2108,7 +2108,7 @@
 	 m2  :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));
 	 nom :=sort (mv_geq LEX_) (mv_shorten(mv_add(mv_mul(!t11',!m1,LEX_),mv_mul(!t21',!m2,LEX_),LEX_),LEX_));
 	 (
-	  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+	  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 	  $ 
 	  (
 	   poly2expanded((!nom),vars)
@@ -2166,11 +2166,11 @@
 
 (*. converts a list of terms to a list of mv_poly .*)
 fun t2d([],_)=[] 
-  | t2d((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars); 
+  | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars); 
 
 (*. same as t2d, this time for expanded forms .*)
 fun t2d_exp([],_)=[]  
-  | t2d_exp((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
+  | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
 
 (*. converts a list of fract terms to a list of their denominators .*)
 fun termlist2denominators [] = ([],[])
@@ -2183,7 +2183,7 @@
 	while length(!xxs)>0 do
 	    (
 	     let 
-		 val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
+		 val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
 	     in
 		 (
 		  xxs:=tl(!xxs);
@@ -2200,11 +2200,11 @@
 
 (*. converts a list of terms to a list of mv_poly .*)
 fun t2d([],_)=[] 
-  | t2d((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars); 
+  | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars); 
 
 (*. same as t2d, this time for expanded forms .*)
 fun t2d_exp([],_)=[]  
-  | t2d_exp((t as (Const("HOL.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
+  | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
 
 (*. converts a list of fract terms to a list of their denominators .*)
 fun termlist2denominators [] = ([],[])
@@ -2217,7 +2217,7 @@
 	while length(!xxs)>0 do
 	    (
 	     let 
-		 val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
+		 val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
 	     in
 		 (
 		  xxs:=tl(!xxs);
@@ -2239,7 +2239,7 @@
 	while length(!xxs)>0 do
 	    (
 	     let 
-		 val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
+		 val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
 	     in
 		 (
 		  xxs:=tl(!xxs);
@@ -2253,7 +2253,7 @@
 (*. reduces all fractions to the least common denominator .*)
 fun com_den(x::xs,denom,den,var)=
     let 
-	val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
+	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));
 	val p3= #1(mv_division(denom,p2,LEX_));
 	val p1var=get_vars(p1');
@@ -2261,10 +2261,10 @@
 	if length(xs)>0 then 
 	    if p3=[(1,mv_null2(var))] then
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		 $ 
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  poly2term(the (term2poly p1' p1var),p1var)
 		  $ 
@@ -2277,10 +2277,10 @@
 		)
 	    else
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		 $ 
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  (
 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -2301,7 +2301,7 @@
 	    if p3=[(1,mv_null2(var))] then
 		(
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  poly2term(the (term2poly p1' p1var),p1var)
 		  $ 
@@ -2312,7 +2312,7 @@
 		 )
 	     else
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  (
 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -2329,7 +2329,7 @@
 (*. same as com_den, this time for expanded forms .*)
 fun com_den_exp(x::xs,denom,den,var)=
     let 
-	val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
+	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));
 	val p3= #1(mv_division(denom,p2,LEX_));
 	val p1var=get_vars(p1');
@@ -2337,10 +2337,10 @@
 	if length(xs)>0 then 
 	    if p3=[(1,mv_null2(var))] then
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
 		 $ 
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  poly2expanded(the(expanded2poly p1' p1var),p1var)
 		  $ 
@@ -2353,10 +2353,10 @@
 		)
 	    else
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		 $ 
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  (
 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -2377,7 +2377,7 @@
 	    if p3=[(1,mv_null2(var))] then
 		(
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  poly2expanded(the(expanded2poly p1' p1var),p1var)
 		  $ 
@@ -2388,7 +2388,7 @@
 		 )
 	     else
 		 (
-		  Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
+		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) 
 		  $ 
 		  (
 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
@@ -2407,7 +2407,7 @@
 (* WN0210???SK brauch ma des überhaupt *)
 fun com_den2(x::xs,denom,den,var)=
     let 
-	val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
+	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));
 	val p3= #1(mv_division(denom,p2,LEX_));
 	val p1var=get_vars(p1');
@@ -2415,13 +2415,13 @@
 	if length(xs)>0 then 
 	    if p3=[(1,mv_null2(var))] then
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 		 poly2term(the(term2poly p1' p1var),p1var) $ 
 		 com_den2(xs,denom,den,var)
 		)
 	    else
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 		 (
 		   let 
 		       val p3'=poly2term(p3,var);
@@ -2451,7 +2451,7 @@
 (* WN0210???SK brauch ma des überhaupt *)
 fun com_den_exp2(x::xs,denom,den,var)=
     let 
-	val (t as Const ("HOL.divide",_) $ p1' $ p2')=x;
+	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));
 	val p3= #1(mv_division(denom,p2,LEX_));
 	val p1var=get_vars p1';
@@ -2459,13 +2459,13 @@
 	if length(xs)>0 then 
 	    if p3=[(1,mv_null2(var))] then
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 		 poly2expanded(the (expanded2poly p1' p1var),p1var) $ 
 		 com_den_exp2(xs,denom,den,var)
 		)
 	    else
 		(
-		 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 		 (
 		   let 
 		       val p3'=poly2expanded(p3,var);
@@ -2644,7 +2644,7 @@
 	val den=factorize_den(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)
     in
 	(
-	 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+	 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 	 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $
 	 poly2term(denom,var)
 	,
@@ -2662,7 +2662,7 @@
 	val den=factorize_den_exp(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)
     in
 	(
-	 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+	 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 	 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $
 	 poly2expanded(denom,var)
 	,
@@ -2673,21 +2673,21 @@
 
 
 (*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)
-fun term2list (t as (Const("HOL.divide",_) $ _ $ _)) = [t]
+fun term2list (t as (Const("Rings.inverse_class.divide",_) $ _ $ _)) = [t]
   | term2list (t as (Const("Atools.pow",_) $ _ $ _)) = 
-    [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+    [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 	  t $ Free("1",HOLogic.realT)
      ]
   | term2list (t as (Free(_,_))) = 
-    [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+    [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 	  t $  Free("1",HOLogic.realT)
      ]
   | term2list (t as (Const("op *",_) $ _ $ _)) = 
-    [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
+    [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ 
 	  t $ Free("1",HOLogic.realT)
      ]
-  | term2list (Const("op +",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
-  | term2list (Const("op -",_) $ t1 $ t2) = 
+  | term2list (Const("Groups.plus_class.plus",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
+  | term2list (Const("Groups.minus_class.minus",_) $ t1 $ t2) = 
     raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
   | term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
 
@@ -2780,7 +2780,7 @@
 	      erls = calc_rat_erls, srls = Erls, (*asm_thm = [],*) 
 	      calc = [], 
 	      rules = 
-	      [Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
+	      [Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
 	       
 	       Thm ("minus_divide_left",
 		    num_str (@{thm minus_divide_left} RS @{thm sym})),
@@ -3001,9 +3001,9 @@
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
-	  calc = [("PLUS"    ,("op +"        ,eval_binop "#add_")),
+	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
-		  ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
+		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  (*asm_thm=[("real_mult_div_cancel2","")],*)
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
@@ -3083,9 +3083,9 @@
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls, 
-	  calc = [("PLUS"    ,("op +"        ,eval_binop "#add_")),
+	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
-		  ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
+		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
 		     normal_form = cancel_ thy, 
@@ -3235,9 +3235,9 @@
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
-	  calc = [("PLUS"    ,("op +"        ,eval_binop "#add_")),
+	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
-		  ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
+		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
 		     normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)
@@ -3383,9 +3383,9 @@
 	  rew_ord=("ord_make_polynomial",
 		   ord_make_polynomial false thy),
 	  erls = rational_erls,
-	  calc = [("PLUS"    ,("op +"        ,eval_binop "#add_")),
+	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
-		  ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
+		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
 	  (*asm_thm=[("real_mult_div_cancel2","")],*)
 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,
@@ -3402,20 +3402,20 @@
 
 (*.the expression contains + - * ^ / only ?.*)
 fun is_ratpolyexp (Free _) = true
-  | is_ratpolyexp (Const ("op +",_) $ Free _ $ Free _) = true
-  | is_ratpolyexp (Const ("op -",_) $ Free _ $ Free _) = true
+  | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
+  | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
   | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true
   | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
-  | is_ratpolyexp (Const ("HOL.divide",_) $ Free _ $ Free _) = true
-  | is_ratpolyexp (Const ("op +",_) $ t1 $ t2) = 
+  | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true
+  | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
-  | is_ratpolyexp (Const ("op -",_) $ t1 $ t2) = 
+  | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
   | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
   | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
-  | is_ratpolyexp (Const ("HOL.divide",_) $ t1 $ t2) = 
+  | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
   | is_ratpolyexp _ = false;
 
@@ -3462,7 +3462,7 @@
 	       Calc ("op <",eval_equ "#less_"),
 	       Thm ("not_false", num_str @{thm not_false}),
 	       Thm ("not_true", num_str @{thm not_true}),
-	       Calc ("op +",eval_binop "#add_")
+	       Calc ("Groups.plus_class.plus",eval_binop "#add_")
 	       ],
       scr = EmptyScr
       }:rls);
@@ -3495,7 +3495,7 @@
 	       (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
 	       Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI}),
 	       (*"1 ^^^ n = 1"*)
-	       Calc ("op +",eval_binop "#add_")
+	       Calc ("Groups.plus_class.plus",eval_binop "#add_")
 	       ],
       scr = EmptyScr
       }:rls);
@@ -3519,7 +3519,7 @@
 	       Thm ("divide_divide_eq_left",
                      num_str @{thm divide_divide_eq_left}),
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
 	       ],
       scr = EmptyScr
       }:rls);
@@ -3695,7 +3695,7 @@
 	       Thm ("divide_divide_eq_left",
                      num_str @{thm divide_divide_eq_left}),
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
 	      
 	       Thm ("rat_power", num_str @{thm rat_power})
 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Root.thy
--- a/src/Tools/isac/Knowledge/Root.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Root.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -168,10 +168,10 @@
       append_rls "Root_crls" Atools_erls 
        [Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
         Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
-        Calc ("HOL.divide",eval_cancel "#divide_e"),
+        Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
         Calc ("Atools.pow" ,eval_binop "#power_"),
-        Calc ("op +", eval_binop "#add_"), 
-        Calc ("op -", eval_binop "#sub_"),
+        Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
+        Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
         Calc ("op *", eval_binop "#mult_"),
         Calc ("op =",eval_equal "#equal_") 
         ];
@@ -180,10 +180,10 @@
       append_rls "Root_erls" Atools_erls 
        [Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
         Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
-        Calc ("HOL.divide",eval_cancel "#divide_e"),
+        Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
         Calc ("Atools.pow" ,eval_binop "#power_"),
-        Calc ("op +", eval_binop "#add_"), 
-        Calc ("op -", eval_binop "#sub_"),
+        Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
+        Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
         Calc ("op *", eval_binop "#mult_"),
         Calc ("op =",eval_equal "#equal_") 
         ];
@@ -251,7 +251,7 @@
 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	       Calc ("op *", eval_binop "#mult_"),
 	       Calc ("Atools.pow", eval_binop "#power_")
 	       ],
@@ -296,10 +296,10 @@
 	       Thm ("add_0_left",num_str @{thm add_0_left}), 
                  (*"0 + z = z"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
-	       Calc ("op -", eval_binop "#sub_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
+	       Calc ("Groups.minus_class.minus", eval_binop "#sub_"), 
 	       Calc ("op *", eval_binop "#mult_"),
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
 	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 	       Calc ("Atools.pow", eval_binop "#power_"),
 
@@ -321,10 +321,10 @@
 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
-	       Calc ("op -", eval_binop "#sub_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
+	       Calc ("Groups.minus_class.minus", eval_binop "#sub_"), 
 	       Calc ("op *", eval_binop "#mult_"),
-	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
+	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
 	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 	       Calc ("Atools.pow", eval_binop "#power_")
 	       ],
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -156,10 +156,10 @@
 	fun coeff_in c v = member op = (vars c) v;
         fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
 	  (* at the moment there is no term like this, but ....*)
-          | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
+          | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
           | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
-          | isnorm (Const ("op -",_) $ _ $ _) v = false
-          | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 
+          | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
+          | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 
                               (is_sqrtTerm_in t2 v)
           | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
  	  | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
@@ -445,10 +445,10 @@
                              (* a+(b+c) = a+b+c *)
                 Thm  ("real_assoc_2",num_str @{thm real_assoc_2}),
                              (* a*(b*c) = a*b*c *)
-                Calc ("op +",eval_binop "#add_"),
-                Calc ("op -",eval_binop "#sub_"),
+                Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+                Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
                 Calc ("op *",eval_binop "#mult_"),
-                Calc ("HOL.divide", eval_cancel "#divide_e"),
+                Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
                 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
                 Calc ("Atools.pow" ,eval_binop "#power_"),
                 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/RootRatEq.thy
--- a/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -43,14 +43,14 @@
 fun is_rootRatAddTerm_in t v = 
     let 
 	fun coeff_in c v = member op = (vars c) v;
-	fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = 
+	fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v = 
             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
-	  | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = 
+	  | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v = 
             (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
 	  | rootadd _ _ = false;
 	fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
 	  (* at the moment there is no term like this, but ....*)
-	  | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = 
+	  | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v = 
 	               if (is_rootTerm_in t3 v) then rootadd t3 v else false
 	  | findrootrat (_ $ t1 $ t2) v = 
             (findrootrat t1 v) orelse (findrootrat t2 v)
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -227,7 +227,7 @@
 	       Calc ("Atools.is'_const",eval_const "#is_const_"),
 	       Calc ("Tools.matches",eval_matches ""),
     
-	       Calc ("op +",eval_binop "#add_"),
+	       Calc ("Groups.plus_class.plus",eval_binop "#add_"),
 	       Calc ("op *",eval_binop "#mult_"),
 	       Calc ("Atools.pow" ,eval_binop "#power_"),
 		    
@@ -272,7 +272,7 @@
 	       Calc ("Test.contains'_root",
 		     eval_contains_root"#contains_root_"),
     
-	       Calc ("op +",eval_binop "#add_"),
+	       Calc ("Groups.plus_class.plus",eval_binop "#add_"),
 	       Calc ("op *",eval_binop "#mult_"),
 	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 	       Calc ("Atools.pow" ,eval_binop "#power_"),
@@ -406,9 +406,9 @@
 	       Thm ("radd_real_const",num_str @{thm radd_real_const}),
 	       (* these 2 rules are invers to distr_div_right wrt. termination.
 		  thus they MUST be done IMMEDIATELY before calc *)
-	       Calc ("op +", eval_binop "#add_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	       Calc ("op *", eval_binop "#mult_"),
-	       Calc ("HOL.divide", eval_cancel "#divide_e"),
+	       Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
 	       Calc ("Atools.pow", eval_binop "#power_"),
 
 	       Thm ("rcollect_right",num_str @{thm rcollect_right}),
@@ -476,7 +476,7 @@
 ML {*
 
 (* association list for calculate_, calculate
-   "op +" etc. not usable in scripts *)
+   "Groups.plus_class.plus" etc. not usable in scripts *)
 val calclist = 
     [
      (*as Tools.ML*)
@@ -484,9 +484,9 @@
      ("matches",("Tools.matches",eval_matches "#matches_")),
      ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),
      (*aus Atools.ML*)
-     ("PLUS"    ,("op +"        ,eval_binop "#add_")),
+     ("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
      ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
-     ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
+     ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
      ("POWER"  ,("Atools.pow"  ,eval_binop "#power_")),
      ("is_const",("Atools.is'_const",eval_const "#is_const_")),
      ("le"      ,("op <"        ,eval_equ "#less_")),
@@ -1295,7 +1295,7 @@
   Rls{id = "make_polytest", preconds = []:term list, 
       rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),
       erls = testerls, srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
@@ -1352,7 +1352,7 @@
 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-	       Calc ("op +", eval_binop "#add_"), 
+	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	       Calc ("op *", eval_binop "#mult_"),
 	       Calc ("Atools.pow", eval_binop "#power_")
 	       ],
@@ -1401,7 +1401,7 @@
   Rls{id = "expand_binomtest", preconds = [], 
       rew_ord = ("termlessI",termlessI),
       erls = testerls, srls = Erls,
-      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
+      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
 	      ("TIMES" , ("op *", eval_binop "#mult_")),
 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
 	      ],
@@ -1452,7 +1452,7 @@
 	Thm ("add_0_left",num_str @{thm add_0_left}),
          (*"0 + z = z"*)
 
-	Calc ("op +", eval_binop "#add_"), 
+	Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	Calc ("op *", eval_binop "#mult_"),
 	Calc ("Atools.pow", eval_binop "#power_"),
         (*	       
@@ -1485,7 +1485,7 @@
 	Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
 	(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-	Calc ("op +", eval_binop "#add_"), 
+	Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
 	Calc ("op *", eval_binop "#mult_"),
 	Calc ("Atools.pow", eval_binop "#power_")
 	],
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/ProgLang/calculate.sml
--- a/src/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -137,22 +137,22 @@
     end;
  (*
 >  val t = (term_of o the o (parse thy)) "#3 + #4";
->  val eval_fn = the (assoc (!eval_list, "op +"));
->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
+>  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
+>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  Syntax.string_of_term (thy2ctxt thy) t';
 >  atomty t';
 > 
 >  val t = (term_of o the o (parse thy)) "(a + #3) + #4";
->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
+>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  Syntax.string_of_term (thy2ctxt thy) t';
 > 
 >  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
+>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  Syntax.string_of_term (thy2ctxt thy) t';
 > 
 >  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
 >  atomty t;
->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
+>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  Syntax.string_of_term (thy2ctxt thy) t';
 >  val it = "#3 + (#4 + a) = #7 + a" : string
 >
@@ -273,15 +273,15 @@
 -------------------------------------------------------------------6.8.02:
 
 > val ct = (the o (parse thy)) "a+#3+#4";
-> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
+> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
 val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")
  
 > val ct = (the o (parse thy)) "#3+(#4+a)";
-> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
+> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")
  
 > val ct = (the o (parse thy)) "a+(#3+#4)+#5";
-> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
+> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
 val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
 
 > val ct = (the o (parse thy)) "#3*(#4*a)";
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/ProgLang/scrtools.sml
--- a/src/Tools/isac/ProgLang/scrtools.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/ProgLang/scrtools.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -389,7 +389,7 @@
     Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
 atomt t; term2str t;
-val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
+val t = rule2stac calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
 atomt t; term2str t;
 val t = rule2stac [] (Rls_ rearrange_assoc);
 atomt t; term2str t;
@@ -406,7 +406,7 @@
 			HOLogic.false_const);
 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
 atomt t; term2str t;
-val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
+val t = rule2stac_inst calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
 atomt t; term2str t;
 val t = rule2stac_inst [] (Rls_ rearrange_assoc);
 atomt t; term2str t;
diff -r e4f42a63d665 -r 3e11e3c2dc42 src/Tools/isac/ProgLang/term.sml
--- a/src/Tools/isac/ProgLang/term.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/src/Tools/isac/ProgLang/term.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -609,10 +609,10 @@
 *)
 
 (*used for calculating built in binary operations in Isabelle2002->Float.ML*)
-(*fun calc "op +"  (n1, n2) = n1+n2
-  | calc "op -"  (n1, n2) = n1-n2
+(*fun calc "Groups.plus_class.plus"  (n1, n2) = n1+n2
+  | calc "Groups.minus_class.minus"  (n1, n2) = n1-n2
   | calc "op *"  (n1, n2) = n1*n2
-  | calc "HOL.divide"(n1, n2) = n1 div n2
+  | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
   | calc "Atools.pow"(n1, n2) = power n1 n2
   | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
 fun calc_equ "op <"  (n1, n2) = n1 < n2
@@ -1163,8 +1163,8 @@
 fun is_atom (Const ("Float.Float",_) $ _) = true
   | is_atom (Const ("ComplexI.I'_'_",_)) = true
   | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
-  | is_atom (Const ("op +",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
-  | is_atom (Const ("op +",_) $ t1 $ 
+  | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
+  | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ 
 		   (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = 
     is_atom t1 andalso is_atom t2
   | is_atom (Const _) = true
@@ -1185,7 +1185,7 @@
 > is_atom t;
 val it = true : bool
 > val t = str2term "1 + 2*I__";
-> val Const ("op +",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
+> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
 *)
 
 (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
@@ -1214,6 +1214,6 @@
     let val T1 = type_of t1
 	val T2 = type_of t2
     in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2])
-       else (Const ("op +", [T1, T2] ---> T1) $ t1 $ t2)
+       else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
     end;
 
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/Interpret/rewtools.sml
--- a/test/Tools/isac/Interpret/rewtools.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/Interpret/rewtools.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -524,10 +524,10 @@
 if contains_rule r1 Test_simplify then ()
 else raise error "rewtools.sml contains_rule Thm";
 
-val r1 = Calc ("op +", eval_binop "#add_");
+val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");
 if contains_rule r1 Test_simplify then ()
 else raise error "rewtools.sml contains_rule Calc";
 
-val r1 = Calc ("op -", eval_binop "#add_");
+val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
 if not (contains_rule r1 Test_simplify) then ()
 else raise error "rewtools.sml contains_rule Calc";
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/Knowledge/biegelinie.sml
--- a/test/Tools/isac/Knowledge/biegelinie.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/Knowledge/biegelinie.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -142,11 +142,11 @@
 				  [(*for asm in nth_Cons_ ...*)
 				   Calc ("op <",eval_equ "#less_"),
 				   (*2nd nth_Cons_ pushes n+-1 into asms*)
-				   Calc("op +", eval_binop "#add_")
+				   Calc("Groups.plus_class.plus", eval_binop "#add_")
 				   ], 
 		srls = Erls, calc = [],
 		rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
-			 Calc("op +", eval_binop "#add_"),
+			 Calc("Groups.plus_class.plus", eval_binop "#add_"),
 			 Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
 			 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
 			 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/Knowledge/diff.sml
--- a/test/Tools/isac/Knowledge/diff.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/Knowledge/diff.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -69,7 +69,7 @@
 		     Calc ("Atools.occurs'_in", eval_occurs_in ""),
 		     Calc ("Tools.matches",eval_matches ""),
 		     
-		     Calc ("op +",eval_binop "#add_"),
+		     Calc ("Groups.plus_class.plus",eval_binop "#add_"),
 		     Calc ("op *",eval_binop "#mult_"),
 		     Calc ("Atools.pow" ,eval_binop "#power_"),
 		     
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/Knowledge/eqsystem.sml
--- a/test/Tools/isac/Knowledge/eqsystem.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/Knowledge/eqsystem.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -88,7 +88,7 @@
 val testrls = append_rls "testrls" e_rls 
 			 [(Thm ("length_Nil_",num_str @{thm length_Nil_})),
 			  (Thm ("length_Cons_",num_str @{thm length_Cons_})),
-			  Calc ("op +", eval_binop "#add_"),
+			  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 			  Calc ("op =",eval_equal "#equal_")
 			  ];
 val SOME (t',_) = rewrite_set_ thy false testrls t;
@@ -725,7 +725,7 @@
 #####  try calc: op <'
 ###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + -1"]
 
-... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)
+... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
 trace_rewrite:=false;
 (*WN051014------------------------------------------------------------------*)
 
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/Knowledge/integrate.sml
--- a/test/Tools/isac/Knowledge/integrate.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/Knowledge/integrate.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -102,7 +102,7 @@
 
 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
 "####1###################################################";
-term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "op +";
+term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "Groups.plus_class.plus";
 "####2###################################################";
 
 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/ProgLang/calculate-float.sml
--- a/test/Tools/isac/ProgLang/calculate-float.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/ProgLang/calculate-float.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -38,7 +38,7 @@
 val thy = Float.thy;
 
 (*.calculate the value of a pair of floats.*)
-val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
+val ((a,b),(c,d)) = calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
 
 
 (*.build the term.*)
@@ -113,7 +113,7 @@
 
 (*.the function evaluating a binary operator.*)
 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
-val SOME (thmid, t) = eval_binop "#add_" "op +" t thy;
+val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" t thy;
 term2str t;
 
 
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/ProgLang/calculate.sml
--- a/test/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 14:49:23 2010 +0200
@@ -17,7 +17,7 @@
 
 (*  [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)),
      ("Nth",("Tools.Nth",fn)),
-   ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)),
+   ("power_",("Atools.pow",fn)),("plus",("Groups.plus_class.plus",fn)),("times",("op *",fn)),
    ("is_const",("Atools.is'_const",fn)),
    ("le",("op <",fn)),("leq",("op <=",fn)),
    ("ident",("Atools.ident",fn))]                                                      *)
@@ -77,9 +77,9 @@
    ("#Find"  ,["realTestFind s_"])
    ],
   {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
-   calc=[("plus"    ,("op +"        ,eval_binop "#add_")),
+   calc=[("plus"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
 	 ("times"   ,("op *"        ,eval_binop "#mult_")),
-	 ("divide_" ,("HOL.divide"  ,eval_cancel "#divide_")),
+	 ("divide_" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_")),
 	 ("power_"  ,("Atools.pow"  ,eval_binop "#power_"))],
    crls=tval_rls, nrls=e_rls(*,
    asm_rls=[],asm_thm=[]*)},
@@ -185,7 +185,7 @@
  trace_rewrite:=true;
  val thy = Test.thy;
  val t = (term_of o the o (parse thy)) "(-4) / 2";
- val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
+ val SOME (_,t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;
  term2str t;
 "-4 / 2 = (-2)";
 (*-------------- but ... *)
diff -r e4f42a63d665 -r 3e11e3c2dc42 test/Tools/isac/Test_Isac.thy
--- a/test/Tools/isac/Test_Isac.thy	Thu Sep 23 12:56:51 2010 +0200
+++ b/test/Tools/isac/Test_Isac.thy	Thu Sep 23 14:49:23 2010 +0200
@@ -81,12 +81,10 @@
 ML {*print_depth 99*}
 
 ML {*
-fun term2str trm = Print_Mode.setmp (Print_Mode.input ::
-        filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
-        (Syntax.string_of_term @{context}) trm;
-val trm = str2term "a+b"; term2str trm;
-val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm;
-"=========================================================";
+str2term "a + b";
+str2term "a - b";
+str2term "a * b";
+str2term "a / b";
 *}
 
 use "Knowledge/integrate.sml";