src/HOL/Library/Nat_Infinity.thy
changeset 29012 9140227dc8c5
parent 28562 4e74209f113e
child 29014 e515f42d1db7
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Fri Dec 05 17:35:22 2008 -0800
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 19:39:53 2008 -0800
     1.3 @@ -146,8 +146,8 @@
     1.4    by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
     1.5  
     1.6  lemma plus_inat_number [simp]:
     1.7 -  "(number_of k \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
     1.8 -    else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
     1.9 +  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
    1.10 +    else if l < Int.Pls then number_of k else number_of (k + l))"
    1.11    unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
    1.12  
    1.13  lemma iSuc_number [simp]: