# HG changeset patch
# User huffman
# Date 1321510530 -3600
# Node ID 787a1a097465391ad2ed4886e723df3c7548ba4f
# Parent  af3690f6bd799f17cdb63c25cf694303a3b4ac34
remove redundant simp rules plus_enat_0

diff -r af3690f6bd79 -r 787a1a097465 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))"