src/ZF/Cardinal.thy
changeset 1401 0c439768f45c
parent 832 ad50a9e74eaf
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Cardinal.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Cardinal.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  Cardinal = OrderType + Fixedpt + Nat + Sum + 
     1.6  consts
     1.7 -  Least            :: "(i=>o) => i"    (binder "LEAST " 10)
     1.8 +  Least            :: (i=>o) => i    (binder "LEAST " 10)
     1.9    eqpoll, lepoll,
    1.10 -          lesspoll :: "[i,i] => o"     (infixl 50)
    1.11 -  cardinal         :: "i=>i"           ("|_|")
    1.12 -  Finite, Card     :: "i=>o"
    1.13 +          lesspoll :: [i,i] => o     (infixl 50)
    1.14 +  cardinal         :: i=>i           ("|_|")
    1.15 +  Finite, Card     :: i=>o
    1.16  
    1.17  defs
    1.18