1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Dec 08 21:33:50 2008 +0100
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Dec 09 11:49:12 2008 -0800
     1.3 @@ -216,6 +216,15 @@
     1.4  lemma mult_iSuc_right: "m * iSuc n = m + m * n"
     1.5    unfolding iSuc_plus_1 by (simp add: ring_simps)
     1.6  
     1.7 +lemma of_nat_eq_Fin: "of_nat n = Fin n"
     1.8 +  apply (induct n)
     1.9 +  apply (simp add: Fin_0)
    1.10 +  apply (simp add: plus_1_iSuc iSuc_Fin)
    1.11 +  done
    1.12 +
    1.13 +instance inat :: semiring_char_0
    1.14 +  by default (simp add: of_nat_eq_Fin)
    1.15 +
    1.16  
    1.17  subsection {* Ordering *}
    1.18