diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu Jun 24 17:51:28 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu Jun 24 17:52:02 2004 +0200
@@ -455,7 +455,7 @@
 
 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
 apply (induct z, simp add: complex_mod complex_cnj complex_mult)
-apply (simp add: power2_eq_square real_abs_def)
+apply (simp add: power2_eq_square abs_if linorder_not_less)
 done
 
 lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
@@ -571,7 +571,7 @@
      complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
 
 
-instance complex :: ringpower
+instance complex :: recpower
 proof
   fix z :: complex
   fix n :: nat
@@ -947,7 +947,7 @@
 test "(a*(b*c)) / ((b::complex)) = (uu::complex)";
 test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)";
 
-(*FIXME: what do we do about this?*)
+FIXME: what do we do about this?
 test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z";
 *)