1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Feb 08 13:20:40 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Fri Feb 09 11:16:05 2018 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4     [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
     1.5      (*		
     1.6       Don't use
     1.7 -     Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
     1.8 +     Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
     1.9       Calc ("Atools.pow" ,eval_binop "#power_"),
    1.10       *)
    1.11      ];
    1.12 @@ -65,7 +65,7 @@
    1.13     [Thm  ("real_assoc_1",num_str @{thm real_assoc_1})
    1.14      (*		
    1.15       Don't use
    1.16 -     Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
    1.17 +     Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
    1.18       Calc ("Atools.pow" ,eval_binop "#power_"),
    1.19       *)
    1.20      ];
    1.21 @@ -86,7 +86,7 @@
    1.22  		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
    1.23  		Calc ("Groups.times_class.times",eval_binop "#mult_"),
    1.24  		(*  Dont use  
    1.25 -		 Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),		
    1.26 +		 Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),		
    1.27  		 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.28  		 *)
    1.29  		Calc ("Atools.pow" ,eval_binop "#power_")