src/ZF/Nat.thy

--- a/src/ZF/Nat.thy	Fri Oct 04 15:23:58 2002 +0200
+++ b/src/ZF/Nat.thy	Fri Oct 04 15:57:32 2002 +0200
@@ -110,6 +110,9 @@
 apply (erule ltD)
 done
 
+lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
+by (induct a rule: nat_induct, auto)
+
 lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
 by (rule Ord_trans [OF succI1], auto)