--- a/src/HOL/Complex/Complex.thy Thu Sep 28 16:01:48 2006 +0200
+++ b/src/HOL/Complex/Complex.thy Thu Sep 28 19:04:13 2006 +0200
@@ -221,7 +221,7 @@
by (simp add: complex_scaleR_def right_distrib)
show "(a + b) *# x = a *# x + b *# x"
by (simp add: complex_scaleR_def left_distrib [symmetric])
- show "(a * b) *# x = a *# b *# x"
+ show "a *# b *# x = (a * b) *# x"
by (simp add: complex_scaleR_def mult_assoc [symmetric])
show "1 *# x = x"
by (simp add: complex_scaleR_def complex_one_def [symmetric])