--- 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