remove redundant simp rules plus_enat_0
authorhuffman
Thu, 17 Nov 2011 07:15:30 +0100
changeset 45539 787a1a097465
parent 45533 af3690f6bd79
child 45540 7f5050fb8821
remove redundant simp rules plus_enat_0
src/HOL/Library/Extended_Nat.thy
--- 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))"