author | huffman |
Thu, 17 Nov 2011 07:15:30 +0100 | |
changeset 45539 | 787a1a097465 |
parent 45533 | af3690f6bd79 |
child 45540 | 7f5050fb8821 |
--- a/src/HOL/Library/Extended_Nat.thy Thu Nov 17 06:04:59 2011 +0100 +++ b/src/HOL/Library/Extended_Nat.thy Thu Nov 17 07:15:30 2011 +0100 @@ -174,11 +174,6 @@ end -lemma plus_enat_0 [simp]: - "0 + (q\<Colon>enat) = q" - "(q\<Colon>enat) + 0 = q" - by (simp_all add: plus_enat_def zero_enat_def split: enat.splits) - lemma plus_enat_number [simp]: "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l else if l < Int.Pls then number_of k else number_of (k + l))"