# HG changeset patch
# User krauss
# Date 1169474928 -3600
# Node ID e1d68715ed09d22d2d8ff96381afd39c1f6be081
# Parent  d0926c4ea65362873152537851c764accd896cb4
Added lemma nat_size[simp]: "size (n::nat) = n"

diff -r d0926c4ea653 -r e1d68715ed09 src/HOL/Nat.thy
--- 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