src/HOL/Library/Product_Vector.thy
changeset 44749 5b1e1432c320
parent 44575 c5e42b8590dd
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Sep 06 07:45:18 2011 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Sep 06 07:48:59 2011 -0700
     1.3 @@ -450,7 +450,7 @@
     1.4    assumes x: "0 \<le> x" and y: "0 \<le> y"
     1.5    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     1.6  apply (rule power2_le_imp_le)
     1.7 -apply (simp add: real_sum_squared_expand x y)
     1.8 +apply (simp add: power2_sum x y)
     1.9  apply (simp add: mult_nonneg_nonneg x y)
    1.10  apply (simp add: x y)
    1.11  done