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.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  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"