src/HOL/Complex.thy

--- a/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Complex.thy	Tue Sep 06 07:48:59 2011 -0700
@@ -321,8 +321,6 @@
 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
   by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
 
-lemmas real_sum_squared_expand = power2_sum [where 'a=real]
-
 lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
   by (cases x) simp