# HG changeset patch
# User haftmann
# Date 1178785310 -7200
# Node ID 0dbcb73bf9bf9f7c280584c8b70da78826eb2620
# Parent  3de2d0b5b89ad6abff0d4b7f8b53ab402031c253
size [nat] is identity

diff -r 3de2d0b5b89a -r 0dbcb73bf9bf src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu May 10 10:21:48 2007 +0200
+++ b/src/HOL/Nat.thy	Thu May 10 10:21:50 2007 +0200
@@ -1266,6 +1266,9 @@
   of_nat_0:   "of_nat 0 = 0"
   of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
 
+lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
+  by (induct n) auto
+
 lemma of_nat_1 [simp]: "of_nat 1 = 1"
   by simp
 
@@ -1342,7 +1345,7 @@
 
 subsection {* Size function *}
 
-lemma nat_size [simp]: "size (n::nat) = n"
+lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
 end