# HG changeset patch
# User huffman
# Date 1228852152 28800
# Node ID ef3adebc6d986474379986da66c9d8356c53d672
# Parent  54d3a31ca0f600fed81dfe50b9c2401c3df20c3d
instance inat :: semiring_char_0

diff -r 54d3a31ca0f6 -r ef3adebc6d98 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Dec 08 21:33:50 2008 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Tue Dec 09 11:49:12 2008 -0800
@@ -216,6 +216,15 @@
 lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   unfolding iSuc_plus_1 by (simp add: ring_simps)
 
+lemma of_nat_eq_Fin: "of_nat n = Fin n"
+  apply (induct n)
+  apply (simp add: Fin_0)
+  apply (simp add: plus_1_iSuc iSuc_Fin)
+  done
+
+instance inat :: semiring_char_0
+  by default (simp add: of_nat_eq_Fin)
+
 
 subsection {* Ordering *}