1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
     1.3 @@ -126,7 +126,7 @@
     1.4  lemmas isCont_euclidean_component [simp] =
     1.5    bounded_linear.isCont [OF bounded_linear_euclidean_component]
     1.6  
     1.7 -lemma euclidean_component_zero: "0 $$ i = 0"
     1.8 +lemma euclidean_component_zero [simp]: "0 $$ i = 0"
     1.9    unfolding euclidean_component_def by (rule inner_zero_right)
    1.10  
    1.11  lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"

     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 23:43:22 2011 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:32:02 2011 -0700
     2.3 @@ -1756,7 +1756,7 @@
     2.4    have Kp: "?K > 0" by arith
     2.5      { assume C: "B < 0"
     2.6        have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
     2.7 -        by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
     2.8 +        by(auto intro!:exI[where x=0])
     2.9        hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
    2.10        with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
    2.11          by (simp add: mult_less_0_iff)

     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
     3.3 @@ -5570,9 +5570,6 @@
     3.4  
     3.5  subsection {* Some properties of a canonical subspace *}
     3.6  
     3.7 -(** move **)
     3.8 -declare euclidean_component_zero[simp]
     3.9 -
    3.10  lemma subspace_substandard:
    3.11    "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
    3.12    unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)