# HG changeset patch
# User huffman
# Date 1308845808 25200
# Node ID d32d72ea3215075b24445353a3bacf20d900c55c
# Parent  cc46a678faafe9e7dff404f850651b3d4ce96b79
instance inat :: number_semiring

diff -r cc46a678faaf -r d32d72ea3215 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Thu Jun 23 09:04:20 2011 -0700
+++ b/src/HOL/Library/Nat_Infinity.thy	Thu Jun 23 09:16:48 2011 -0700
@@ -240,6 +240,12 @@
   apply (simp add: plus_1_iSuc iSuc_Fin)
   done
 
+instance inat :: number_semiring
+proof
+  fix n show "number_of (int n) = (of_nat n :: inat)"
+    unfolding number_of_inat_def number_of_int of_nat_id of_nat_eq_Fin ..
+qed
+
 instance inat :: semiring_char_0 proof
   have "inj Fin" by (rule injI) simp
   then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)