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