src/HOL/Library/Product_Vector.thy
changeset 44126 ce44e70d0c47
parent 44066 d74182c93f04
child 44127 7b57b9295d98
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:30:00 2011 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:42:07 2011 -0700
     1.3 @@ -453,9 +453,9 @@
     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 add_nonneg_nonneg x y)
     1.8 +apply (simp add: real_sum_squared_expand x y)
     1.9  apply (simp add: mult_nonneg_nonneg x y)
    1.10 -apply (simp add: add_nonneg_nonneg x y)
    1.11 +apply (simp add: x y)
    1.12  done
    1.13  
    1.14  lemma bounded_linear_Pair: