1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Tue Sep 28 10:01:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Tue Sep 28 10:10:26 2010 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  		  Thm ("sqrt_conv", num_str @{thm sqrt_conv}),
     1.5  		  Thm ("root_conv", num_str @{thm root_conv}),
     1.6  		  Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}),
     1.7 -		  Calc ("op *", eval_binop "#mult_"),
     1.8 +		  Calc ("Groups.times_class.times", eval_binop "#mult_"),
     1.9  		  Thm ("rat_mult",num_str @{thm rat_mult}),
    1.10  		  (*a / b * (c / d) = a * c / (b * d)*)
    1.11  		  Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
    1.12 @@ -167,7 +167,7 @@
    1.13  		  (*?x * (?y / ?z) = ?x * ?y / ?z*)
    1.14  		  Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
    1.15  		  (*?y / ?z * ?x = ?y * ?x / ?z*)
    1.16 -		  Calc ("op *", eval_binop "#mult_")
    1.17 +		  Calc ("Groups.times_class.times", eval_binop "#mult_")
    1.18  		 ],
    1.19  	 scr = EmptyScr};
    1.20