remove redundant simp rules plus_enat_0
authorhuffman
Thu Nov 17 07:15:30 2011 +0100 (2011-11-17)
changeset 45539787a1a097465
parent 45533 af3690f6bd79
child 45540 7f5050fb8821
remove redundant simp rules plus_enat_0
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Nov 17 06:04:59 2011 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Nov 17 07:15:30 2011 +0100
     1.3 @@ -174,11 +174,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma plus_enat_0 [simp]:
     1.8 -  "0 + (q\<Colon>enat) = q"
     1.9 -  "(q\<Colon>enat) + 0 = q"
    1.10 -  by (simp_all add: plus_enat_def zero_enat_def split: enat.splits)
    1.11 -
    1.12  lemma plus_enat_number [simp]:
    1.13    "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
    1.14      else if l < Int.Pls then number_of k else number_of (k + l))"