| changeset 0 | a5a9c433f639 |
| child 30 | d49df4181f0d |
| -1:000000000000 | 0:a5a9c433f639 |
|---|---|
1 (* Title: ZF/ordinal.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Ordinals in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 Ord = WF + |
|
10 consts |
|
11 Memrel :: "i=>i" |
|
12 Transset,Ord :: "i=>o" |
|
13 |
|
14 rules |
|
15 Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }" |
|
16 Transset_def "Transset(i) == ALL x:i. x<=i" |
|
17 Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))" |
|
18 |
|
19 end |