src/HOL/Library/Nat_Infinity.thy
changeset 25112 98824cc791c0
parent 23315 df3a7e9ebadb
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    by (simp add: inat_defs split:inat_splits)
     1.5  
     1.6  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
     1.7 -  by (simp add: inat_defs split:inat_splits)
     1.8 +  by (simp add: neq0_conv inat_defs split:inat_splits)
     1.9  
    1.10  lemma i0_iless_iSuc [simp]: "0 < iSuc n"
    1.11    by (simp add: inat_defs split:inat_splits)