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