Added lemma nat_size[simp]: "size (n::nat) = n"

--- a/src/HOL/Nat.thy	Mon Jan 22 00:40:29 2007 +0100
+++ b/src/HOL/Nat.thy	Mon Jan 22 15:08:48 2007 +0100
@@ -1305,4 +1305,10 @@
 by (simp del: of_nat_add
 	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
 
+
+subsection {* Size function *}
+
+lemma nat_size[simp]: "size (n::nat) = n"
+  by (induct n) simp_all
+
 end