1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Tue Sep 28 10:01:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Tue Sep 28 10:10:26 2010 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4  
     1.5  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
     1.6  (*("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
     1.7 -  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
     1.8 +  ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
     1.9    ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)
    1.10  
    1.11  (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
    1.12 @@ -318,7 +318,7 @@
    1.13  > term2str t;
    1.14  val it = "-1 + 2 = 1"
    1.15  > val t = str2term "-1 * (-1 * a)";
    1.16 -> val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
    1.17 +> val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
    1.18  > term2str t;
    1.19  val it = "-1 * (-1 * a) = 1 * a"*)
    1.20  
    1.21 @@ -560,7 +560,7 @@
    1.22  
    1.23  val list_rls = 
    1.24      append_rls "list_rls" list_rls
    1.25 -	       [Calc ("op *",eval_binop "#mult_"),
    1.26 +	       [Calc ("Groups.times_class.times",eval_binop "#mult_"),
    1.27  		Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
    1.28  		Calc ("op <",eval_equ "#less_"),
    1.29  		Calc ("op <=",eval_equ "#less_equal_"),
    1.30 @@ -593,7 +593,7 @@
    1.31  		Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
    1.32  		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.33  		Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
    1.34 -		Calc ("op *",eval_binop "#mult_")
    1.35 +		Calc ("Groups.times_class.times",eval_binop "#mult_")
    1.36  		];
    1.37  
    1.38  val Atools_erls = 
    1.39 @@ -710,7 +710,7 @@
    1.40      ("equal"    ,("op =",eval_equal "#equal_")),
    1.41      ("PLUS"     ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
    1.42      ("MINUS"    ,("Groups.minus_class.minus",eval_binop "#sub_")),
    1.43 -    ("TIMES"    ,("op *"        ,eval_binop "#mult_")),
    1.44 +    ("TIMES"    ,("Groups.times_class.times"        ,eval_binop "#mult_")),
    1.45      ("DIVIDE"  ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),
    1.46      ("POWER"   ,("Atools.pow"  ,eval_binop "#power_")),
    1.47      ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))