diff -r a34d89ce6097 -r 6616e6c53d48 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Nat.thy	Tue May 27 11:39:03 2003 +0200
@@ -38,12 +38,13 @@
   Gt :: i
     "Gt == {<x,y>:nat*nat. y < x}"
 
-  less_than :: "i=>i"
-    "less_than(n) == {i:nat.  i<n}"
-
   greater_than :: "i=>i"
     "greater_than(n) == {i:nat. n < i}"
 
+text{*No need for a less-than operator: a natural number is its list of
+predecessors!*}
+
+
 lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
 apply (rule bnd_monoI)
 apply (cut_tac infinity, blast, blast) 
@@ -281,6 +282,14 @@
 lemma nat_nonempty [simp]: "nat ~= 0"
 by blast
 
+text{*A natural number is the set of its predecessors*}
+lemma nat_eq_Collect_lt: "i \<in> nat ==> {j\<in>nat. j<i} = i"
+apply (rule equalityI)
+apply (blast dest: ltD)  
+apply (auto simp add: Ord_mem_iff_lt)
+apply (blast intro: lt_trans) 
+done
+
 
 ML
 {*
@@ -288,7 +297,6 @@
 val Lt_def = thm "Lt_def";
 val Ge_def = thm "Ge_def";
 val Gt_def = thm "Gt_def";
-val less_than_def = thm "less_than_def";
 val greater_than_def = thm "greater_than_def";
 
 val nat_bnd_mono = thm "nat_bnd_mono";