--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Cardinal.thy	Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,33 @@
+(*  Title: 	ZF/Cardinal.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Cardinals in Zermelo-Fraenkel Set Theory 
+*)
+
+Cardinal = OrderType + Fixedpt + Nat + Sum + 
+consts
+  Least            :: "(i=>o) => i"    (binder "LEAST " 10)
+  eqpoll, lepoll   :: "[i,i] => o"     (infixl 50)
+  "cardinal"       :: "i=>i"           ("|_|")
+  Card             :: "i=>o"
+
+  swap       :: "[i,i,i]=>i"     (*not used; useful??*)
+
+rules
+
+  (*least ordinal operator*)
+  Least_def  "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
+
+  eqpoll_def "A eqpoll B == EX f. f: bij(A,B)"
+
+  lepoll_def "A lepoll B == EX f. f: inj(A,B)"
+
+  cardinal_def "|A| == LEAST i. i eqpoll A"
+
+  Card_def     "Card(i) == ( i = |i| )"
+
+  swap_def   "swap(A,x,y) == (lam z:A. if(z=x, y, if(z=y, x, z)))"
+
+end