1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 09:01:09 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 11:48:42 2010 +0200
     1.3 @@ -179,9 +179,6 @@
     1.4  
     1.5  subsection{* Basic componentwise operations on vectors. *}
     1.6  
     1.7 -lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"
     1.8 -  using one_le_card_finite by auto
     1.9 -
    1.10  instantiation cart :: (times,finite) times
    1.11  begin
    1.12    definition vector_mult_def : "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"