1.1 --- a/src/HOL/RealVector.thy	Fri Aug 20 17:46:55 2010 +0200
     1.2 +++ b/src/HOL/RealVector.thy	Fri Aug 20 17:46:56 2010 +0200
     1.3 @@ -270,6 +270,10 @@
     1.4  lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
     1.5  by (simp add: of_real_def)
     1.6  
     1.7 +lemma inj_of_real:
     1.8 +  "inj of_real"
     1.9 +  by (auto intro: injI)
    1.10 +
    1.11  lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
    1.12  
    1.13  lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
    1.14 @@ -291,13 +295,11 @@
    1.15  by (simp add: number_of_eq)
    1.16  
    1.17  text{*Every real algebra has characteristic zero*}
    1.18 +
    1.19  instance real_algebra_1 < ring_char_0
    1.20  proof
    1.21 -  fix m n :: nat
    1.22 -  have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
    1.23 -    by (simp only: of_real_eq_iff of_nat_eq_iff)
    1.24 -  thus "(of_nat m = (of_nat n::'a)) = (m = n)"
    1.25 -    by (simp only: of_real_of_nat_eq)
    1.26 +  from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp)
    1.27 +  then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def)
    1.28  qed
    1.29  
    1.30  instance real_field < field_char_0 ..