1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -156,10 +156,10 @@
     1.4  	fun coeff_in c v = member op = (vars c) v;
     1.5          fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
     1.6  	  (* at the moment there is no term like this, but ....*)
     1.7 -          | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
     1.8 +          | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
     1.9            | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
    1.10 -          | isnorm (Const ("op -",_) $ _ $ _) v = false
    1.11 -          | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 
    1.12 +          | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
    1.13 +          | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 
    1.14                                (is_sqrtTerm_in t2 v)
    1.15            | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
    1.16   	  | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
    1.17 @@ -445,10 +445,10 @@
    1.18                               (* a+(b+c) = a+b+c *)
    1.19                  Thm  ("real_assoc_2",num_str @{thm real_assoc_2}),
    1.20                               (* a*(b*c) = a*b*c *)
    1.21 -                Calc ("op +",eval_binop "#add_"),
    1.22 -                Calc ("op -",eval_binop "#sub_"),
    1.23 +                Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.24 +                Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
    1.25                  Calc ("op *",eval_binop "#mult_"),
    1.26 -                Calc ("HOL.divide", eval_cancel "#divide_e"),
    1.27 +                Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
    1.28                  Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.29                  Calc ("Atools.pow" ,eval_binop "#power_"),
    1.30                  Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),