1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4  	       Calc ("Atools.is'_const",eval_const "#is_const_"),
     1.5  	       Calc ("Tools.matches",eval_matches ""),
     1.6      
     1.7 -	       Calc ("op +",eval_binop "#add_"),
     1.8 +	       Calc ("Groups.plus_class.plus",eval_binop "#add_"),
     1.9  	       Calc ("op *",eval_binop "#mult_"),
    1.10  	       Calc ("Atools.pow" ,eval_binop "#power_"),
    1.11  		    
    1.12 @@ -272,7 +272,7 @@
    1.13  	       Calc ("Test.contains'_root",
    1.14  		     eval_contains_root"#contains_root_"),
    1.15      
    1.16 -	       Calc ("op +",eval_binop "#add_"),
    1.17 +	       Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.18  	       Calc ("op *",eval_binop "#mult_"),
    1.19  	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.20  	       Calc ("Atools.pow" ,eval_binop "#power_"),
    1.21 @@ -406,9 +406,9 @@
    1.22  	       Thm ("radd_real_const",num_str @{thm radd_real_const}),
    1.23  	       (* these 2 rules are invers to distr_div_right wrt. termination.
    1.24  		  thus they MUST be done IMMEDIATELY before calc *)
    1.25 -	       Calc ("op +", eval_binop "#add_"), 
    1.26 +	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.27  	       Calc ("op *", eval_binop "#mult_"),
    1.28 -	       Calc ("HOL.divide", eval_cancel "#divide_e"),
    1.29 +	       Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
    1.30  	       Calc ("Atools.pow", eval_binop "#power_"),
    1.31  
    1.32  	       Thm ("rcollect_right",num_str @{thm rcollect_right}),
    1.33 @@ -476,7 +476,7 @@
    1.34  ML {*
    1.35  
    1.36  (* association list for calculate_, calculate
    1.37 -   "op +" etc. not usable in scripts *)
    1.38 +   "Groups.plus_class.plus" etc. not usable in scripts *)
    1.39  val calclist = 
    1.40      [
    1.41       (*as Tools.ML*)
    1.42 @@ -484,9 +484,9 @@
    1.43       ("matches",("Tools.matches",eval_matches "#matches_")),
    1.44       ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),
    1.45       (*aus Atools.ML*)
    1.46 -     ("PLUS"    ,("op +"        ,eval_binop "#add_")),
    1.47 +     ("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
    1.48       ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
    1.49 -     ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),
    1.50 +     ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
    1.51       ("POWER"  ,("Atools.pow"  ,eval_binop "#power_")),
    1.52       ("is_const",("Atools.is'_const",eval_const "#is_const_")),
    1.53       ("le"      ,("op <"        ,eval_equ "#less_")),
    1.54 @@ -1295,7 +1295,7 @@
    1.55    Rls{id = "make_polytest", preconds = []:term list, 
    1.56        rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),
    1.57        erls = testerls, srls = Erls,
    1.58 -      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
    1.59 +      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
    1.60  	      ("TIMES" , ("op *", eval_binop "#mult_")),
    1.61  	      ("POWER", ("Atools.pow", eval_binop "#power_"))
    1.62  	      ],
    1.63 @@ -1352,7 +1352,7 @@
    1.64  	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
    1.65  	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    1.66  
    1.67 -	       Calc ("op +", eval_binop "#add_"), 
    1.68 +	       Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.69  	       Calc ("op *", eval_binop "#mult_"),
    1.70  	       Calc ("Atools.pow", eval_binop "#power_")
    1.71  	       ],
    1.72 @@ -1401,7 +1401,7 @@
    1.73    Rls{id = "expand_binomtest", preconds = [], 
    1.74        rew_ord = ("termlessI",termlessI),
    1.75        erls = testerls, srls = Erls,
    1.76 -      calc = [("PLUS"  , ("op +", eval_binop "#add_")), 
    1.77 +      calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
    1.78  	      ("TIMES" , ("op *", eval_binop "#mult_")),
    1.79  	      ("POWER", ("Atools.pow", eval_binop "#power_"))
    1.80  	      ],
    1.81 @@ -1452,7 +1452,7 @@
    1.82  	Thm ("add_0_left",num_str @{thm add_0_left}),
    1.83           (*"0 + z = z"*)
    1.84  
    1.85 -	Calc ("op +", eval_binop "#add_"), 
    1.86 +	Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.87  	Calc ("op *", eval_binop "#mult_"),
    1.88  	Calc ("Atools.pow", eval_binop "#power_"),
    1.89          (*	       
    1.90 @@ -1485,7 +1485,7 @@
    1.91  	Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 
    1.92  	(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
    1.93  
    1.94 -	Calc ("op +", eval_binop "#add_"), 
    1.95 +	Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.96  	Calc ("op *", eval_binop "#mult_"),
    1.97  	Calc ("Atools.pow", eval_binop "#power_")
    1.98  	],