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