src/ZF/Ordinal.thy
changeset 753 ec86863e87c8
parent 435 ca5356bd315a
child 852 664052e3cf66
     1.1 --- a/src/ZF/Ordinal.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/Ordinal.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -17,12 +17,11 @@
     1.4  translations
     1.5    "x le y"      == "x < succ(y)"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9    Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    1.10    Transset_def	"Transset(i) == ALL x:i. x<=i"
    1.11    Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
    1.12    lt_def        "i<j         == i:j & Ord(j)"
    1.13    Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    1.14  
    1.15 -
    1.16  end