# HG changeset patch
# User lcp
# Date 788196759 -3600
# Node ID ad50a9e74eaf890ba79d44b9ce163b910e01d1fc
# Parent  60d850cc5fe62d16c41027fd0be9c9a4df27f32e
Added Krzysztof's constants lesspoll and Finite

diff -r 60d850cc5fe6 -r ad50a9e74eaf src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Fri Dec 23 16:32:02 1994 +0100
+++ b/src/ZF/Cardinal.thy	Fri Dec 23 16:32:39 1994 +0100
@@ -9,25 +9,26 @@
 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??*)
+  eqpoll, lepoll,
+          lesspoll :: "[i,i] => o"     (infixl 50)
+  cardinal         :: "i=>i"           ("|_|")
+  Finite, Card     :: "i=>o"
 
 defs
 
   (*least ordinal operator*)
-  Least_def  "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
+  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)"
+  eqpoll_def    "A eqpoll B == EX f. f: bij(A,B)"
 
-  lepoll_def "A lepoll B == EX f. f: inj(A,B)"
+  lepoll_def    "A lepoll B == EX f. f: inj(A,B)"
 
-  cardinal_def "|A| == LEAST i. i eqpoll A"
+  lesspoll_def  "A lesspoll B == A lepoll B & ~(A eqpoll B)"
+
+  Finite_def    "Finite(A) == EX n:nat. A eqpoll n"
 
-  Card_def     "Card(i) == ( i = |i| )"
+  cardinal_def  "|A| == LEAST i. i eqpoll A"
 
-  swap_def   "swap(A,x,y) == (lam z:A. if(z=x, y, if(z=y, x, z)))"
+  Card_def      "Card(i) == (i = |i|)"
 
 end