# HG changeset patch
# User lcp
# Date 749838425 -3600
# Node ID b429d6a658ae06f2d1f8ffb257f15bbc2cbe252f
# Parent  0e152fe9571e55bd1d62fec35b176493551e700b
Retry of the previous commit (network outage)

diff -r 0e152fe9571e -r b429d6a658ae src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Tue Oct 05 17:15:28 1993 +0100
+++ b/src/ZF/Univ.thy	Tue Oct 05 17:27:05 1993 +0100
@@ -21,7 +21,7 @@
     "Vset(x)"   == 	"Vfrom(0,x)"
 
 rules
-    Limit_def   "Limit(i) == Ord(i) & 0:i & (ALL y:i. succ(y): i)"
+    Limit_def   "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
 
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
 
diff -r 0e152fe9571e -r b429d6a658ae src/ZF/univ.thy
--- a/src/ZF/univ.thy	Tue Oct 05 17:15:28 1993 +0100
+++ b/src/ZF/univ.thy	Tue Oct 05 17:27:05 1993 +0100
@@ -21,7 +21,7 @@
     "Vset(x)"   == 	"Vfrom(0,x)"
 
 rules
-    Limit_def   "Limit(i) == Ord(i) & 0:i & (ALL y:i. succ(y): i)"
+    Limit_def   "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
 
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"