1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Nov 27 17:44:36 2010 -0800
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 28 15:20:51 2010 +0100
     1.3 @@ -1300,7 +1300,7 @@
     1.4    shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
     1.5    and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
     1.6    unfolding  infnorm_set_image_cart
     1.7 -  by (auto intro: finite_imageI)
     1.8 +  by auto
     1.9  
    1.10  lemma component_le_infnorm_cart:
    1.11    shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"