diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Complex.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -288,8 +288,6 @@
 
 instance proof
   fix r :: real and x y :: complex and S :: "complex set"
-  show "0 \<le> norm x"
-    by (induct x) simp
   show "(norm x = 0) = (x = 0)"
     by (induct x) simp
   show "norm (x + y) \<le> norm x + norm y"