diff -r 000000000000 -r a5a9c433f639 src/ZF/ord.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ord.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,19 @@
+(*  Title: 	ZF/ordinal.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Ordinals in Zermelo-Fraenkel Set Theory 
+*)
+
+Ord = WF +
+consts
+    Memrel      	::      "i=>i"
+    Transset,Ord        ::      "i=>o"
+
+rules
+  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))"
+
+end