1.1 --- a/src/Tools/isac/Knowledge/Root.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -168,10 +168,10 @@
     1.4        append_rls "Root_crls" Atools_erls 
     1.5         [Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
     1.6          Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
     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 -        Calc ("op +", eval_binop "#add_"), 
    1.11 -        Calc ("op -", eval_binop "#sub_"),
    1.12 +        Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.13 +        Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
    1.14          Calc ("op *", eval_binop "#mult_"),
    1.15          Calc ("op =",eval_equal "#equal_") 
    1.16          ];
    1.17 @@ -180,10 +180,10 @@
    1.18        append_rls "Root_erls" Atools_erls 
    1.19         [Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
    1.20          Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
    1.21 -        Calc ("HOL.divide",eval_cancel "#divide_e"),
    1.22 +        Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
    1.23          Calc ("Atools.pow" ,eval_binop "#power_"),
    1.24 -        Calc ("op +", eval_binop "#add_"), 
    1.25 -        Calc ("op -", eval_binop "#sub_"),
    1.26 +        Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.27 +        Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
    1.28          Calc ("op *", eval_binop "#mult_"),
    1.29          Calc ("op =",eval_equal "#equal_") 
    1.30          ];
    1.31 @@ -251,7 +251,7 @@
    1.32  	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
    1.33  	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    1.34  
    1.35 -	       Calc ("op +", eval_binop "#add_"), 
    1.36 +	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.37  	       Calc ("op *", eval_binop "#mult_"),
    1.38  	       Calc ("Atools.pow", eval_binop "#power_")
    1.39  	       ],
    1.40 @@ -296,10 +296,10 @@
    1.41  	       Thm ("add_0_left",num_str @{thm add_0_left}), 
    1.42                   (*"0 + z = z"*)
    1.43  
    1.44 -	       Calc ("op +", eval_binop "#add_"), 
    1.45 -	       Calc ("op -", eval_binop "#sub_"), 
    1.46 +	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.47 +	       Calc ("Groups.minus_class.minus", eval_binop "#sub_"), 
    1.48  	       Calc ("op *", eval_binop "#mult_"),
    1.49 -	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
    1.50 +	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
    1.51  	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.52  	       Calc ("Atools.pow", eval_binop "#power_"),
    1.53  
    1.54 @@ -321,10 +321,10 @@
    1.55  	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
    1.56  	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    1.57  
    1.58 -	       Calc ("op +", eval_binop "#add_"), 
    1.59 -	       Calc ("op -", eval_binop "#sub_"), 
    1.60 +	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.61 +	       Calc ("Groups.minus_class.minus", eval_binop "#sub_"), 
    1.62  	       Calc ("op *", eval_binop "#mult_"),
    1.63 -	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
    1.64 +	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
    1.65  	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.66  	       Calc ("Atools.pow", eval_binop "#power_")
    1.67  	       ],