1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed May 27 21:46:50 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu May 28 09:46:43 2009 +0200
     1.3 @@ -109,10 +109,10 @@
     1.4  
     1.5  text{* Also the scalar-vector multiplication. *}
     1.6  
     1.7 -definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
     1.8 +definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
     1.9    where "c *s x = (\<chi> i. c * (x$i))"
    1.10  
    1.11 -text{* Constant Vectors *}
    1.12 +text{* Constant Vectors *} 
    1.13  
    1.14  definition "vec x = (\<chi> i. x)"
    1.15  

     2.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Wed May 27 21:46:50 2009 -0700
     2.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 09:46:43 2009 +0200
     2.3 @@ -4601,8 +4601,8 @@
     2.4      def f == "\<lambda>n::nat. x + (inverse (real n + 1)) *s (?c - x)"
     2.5      { fix n assume fn:"f n < b \<longrightarrow> a < f n \<longrightarrow> f n = x" and xc:"x \<noteq> ?c"
     2.6        have *:"0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1" unfolding inverse_le_1_iff by auto
     2.7 -      have "inverse (real n + 1) *s (1 / 2) *s (a + b) + (1 - inverse (real n + 1)) *s x =
     2.8 -	x + inverse (real n + 1) *s ((1 / 2) *s (a + b) - x)" by (auto simp add: vector_ssub_ldistrib vector_add_ldistrib field_simps vector_sadd_rdistrib[THEN sym])
     2.9 +      have "(inverse (real n + 1)) *s ((1 / 2) *s (a + b)) + (1 - inverse (real n + 1)) *s x =
    2.10 +	x + (inverse (real n + 1)) *s ((1 / 2 *s (a + b)) - x)" by (auto simp add: vector_ssub_ldistrib vector_add_ldistrib field_simps vector_sadd_rdistrib[THEN sym])
    2.11        hence "f n < b" and "a < f n" using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *] unfolding f_def by auto
    2.12        hence False using fn unfolding f_def using xc by(auto simp add: vector_mul_lcancel vector_ssub_ldistrib)  }
    2.13      moreover