src/ZF/Ordinal.thy
 author wenzelm Thu Jan 23 10:40:21 1997 +0100 (1997-01-23) changeset 2539 ddd22ceee8cc parent 2469 b50b8c0eec01 child 2540 ba8311047f18 permissions -rw-r--r--
turned some consts into syntax;
```     1 (*  Title:      ZF/Ordinal.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 Ordinals in Zermelo-Fraenkel Set Theory
```
```     7 *)
```
```     8
```
```     9 Ordinal = WF + Bool + equalities +
```
```    10 consts
```
```    11   Memrel        :: i=>i
```
```    12   Transset,Ord  :: i=>o
```
```    13   "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
```
```    14   Limit         :: i=>o
```
```    15
```
```    16 syntax
```
```    17   "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
```
```    18
```
```    19 translations
```
```    20   "x le y"      == "x < succ(y)"
```
```    21
```
```    22 defs
```
```    23   Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
```
```    24   Transset_def  "Transset(i) == ALL x:i. x<=i"
```
```    25   Ord_def       "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
```
```    26   lt_def        "i<j         == i:j & Ord(j)"
```
```    27   Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
```
```    28
```
```    29 end
```