author  clasohm 
Thu, 16 Sep 1993 12:20:38 +0200  
changeset 0  a5a9c433f639 
child 30  d49df4181f0d 
permissions  rwrr 
0  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 ZermeloFraenkel 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 