1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 20 17:46:55 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 20 17:46:56 2010 +0200
     1.3 @@ -346,15 +346,15 @@
     1.4  lemma one_index[simp]:
     1.5    "(1 :: 'a::one ^'n)$i = 1" by vector
     1.6  
     1.7 -instance cart :: (semiring_char_0,finite) semiring_char_0
     1.8 -proof (intro_classes)
     1.9 -  fix m n ::nat
    1.10 -  show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
    1.11 -    by (simp add: Cart_eq of_nat_index)
    1.12 +instance cart :: (semiring_char_0, finite) semiring_char_0
    1.13 +proof
    1.14 +  fix m n :: nat
    1.15 +  show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
    1.16 +    by (auto intro!: injI simp add: Cart_eq of_nat_index)
    1.17  qed
    1.18  
    1.19 -instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes
    1.20 -instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes
    1.21 +instance cart :: (comm_ring_1,finite) comm_ring_1 ..
    1.22 +instance cart :: (ring_char_0,finite) ring_char_0 ..
    1.23  
    1.24  instance cart :: (real_vector,finite) real_vector ..
    1.25