# HG changeset patch
# User huffman
# Date 1315321228 25200
# Node ID 5b11f36fcacb1a6f8d4135bbf9e5c6649daae348
# Parent  5b1e1432c3201ea332a5c4033738c1f83a73a7e2
remove duplicate copy of lemma sqrt_add_le_add_sqrt

diff -r 5b1e1432c320 -r 5b11f36fcacb src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:48:59 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 08:00:28 2011 -0700
@@ -415,16 +415,6 @@
   from power2_le_imp_le[OF th yz] show ?thesis .
 qed
 
-text {* TODO: move to NthRoot *}
-lemma sqrt_add_le_add_sqrt:
-  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: power2_sum x y)
-apply (simp add: mult_nonneg_nonneg x y)
-apply (simp add: x y)
-done
-
 subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
 
 definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where