1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4     [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
     1.5      (*		
     1.6       Don't use
     1.7 -     Calc ("HOL.divide", eval_cancel "#divide_e"),
     1.8 +     Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
     1.9       Calc ("Atools.pow" ,eval_binop "#power_"),
    1.10       *)
    1.11      ];
    1.12 @@ -66,7 +66,7 @@
    1.13     [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
    1.14      (*		
    1.15       Don't use
    1.16 -     Calc ("HOL.divide", eval_cancel "#divide_e"),
    1.17 +     Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
    1.18       Calc ("Atools.pow" ,eval_binop "#power_"),
    1.19       *)
    1.20      ];
    1.21 @@ -84,11 +84,11 @@
    1.22         (*asm_thm = [],*)
    1.23         rules = [
    1.24  		Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),
    1.25 -		Calc ("op +",eval_binop "#add_"),
    1.26 -		Calc ("op -",eval_binop "#sub_"),
    1.27 +		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.28 +		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
    1.29  		Calc ("op *",eval_binop "#mult_"),
    1.30  		(*  Dont use  
    1.31 -		 Calc ("HOL.divide", eval_cancel "#divide_e"),		
    1.32 +		 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),		
    1.33  		 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.34  		 *)
    1.35  		Calc ("Atools.pow" ,eval_binop "#power_")