--- a/NEWS Tue Sep 06 07:45:18 2011 -0700
+++ b/NEWS Tue Sep 06 07:48:59 2011 -0700
@@ -276,6 +276,7 @@
real_squared_diff_one_factored ~> square_diff_one_factored
realpow_two_diff ~> square_diff_square_factored
reals_complete2 ~> complete_real
+ real_sum_squared_expand ~> power2_sum
exp_ln_eq ~> ln_unique
expi_add ~> exp_add
expi_zero ~> exp_zero
--- 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
--- a/src/HOL/Library/Product_Vector.thy Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy Tue Sep 06 07:48:59 2011 -0700
@@ -450,7 +450,7 @@
assumes x: "0 \<le> x" and y: "0 \<le> y"
shows "sqrt (x + y) \<le> sqrt x + sqrt y"
apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand x y)
+apply (simp add: power2_sum x y)
apply (simp add: mult_nonneg_nonneg x y)
apply (simp add: x y)
done
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Sep 06 07:48:59 2011 -0700
@@ -420,7 +420,7 @@
assumes x: "0 \<le> x" and y: "0 \<le> y"
shows "sqrt (x + y) \<le> sqrt x + sqrt y"
apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand x y)
+apply (simp add: power2_sum x y)
apply (simp add: mult_nonneg_nonneg x y)
apply (simp add: x y)
done