src/HOL/Multivariate_Analysis/Linear_Algebra.thy
 changeset 44142 8e27e0177518 parent 44133 691c52e900ca child 44166 d12d89a66742
```     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 10 17:02:03 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 10 18:02:16 2011 -0700
1.3 @@ -641,9 +641,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.8 +apply (simp add: real_sum_squared_expand x y)
1.9  apply (simp add: mult_nonneg_nonneg x y)
1.11 +apply (simp add: x y)
1.12  done
1.13
1.14  subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
1.15 @@ -2319,7 +2319,7 @@
1.16    shows "x = 0"
1.17    using fB ifB fi xsB fx
1.18  proof(induct arbitrary: x rule: finite_induct[OF fB])
1.19 -  case 1 thus ?case by (auto simp add:  span_empty)
1.20 +  case 1 thus ?case by auto
1.21  next
1.22    case (2 a b x)
1.23    have fb: "finite b" using "2.prems" by simp
1.24 @@ -2372,7 +2372,7 @@
1.25             \<and> (\<forall>x\<in> B. g x = f x)"
1.26  using ib fi
1.27  proof(induct rule: finite_induct[OF fi])
1.28 -  case 1 thus ?case by (auto simp add: span_empty)
1.29 +  case 1 thus ?case by auto
1.30  next
1.31    case (2 a b)
1.32    from "2.prems" "2.hyps" have ibf: "independent b" "finite b"
```