src/ZF/Ordinal.thy
changeset 1401 0c439768f45c
parent 852 664052e3cf66
child 1478 2b8c2a7547ab
equal deleted inserted replaced
1400:5d909faf0e04 1401:0c439768f45c
     6 Ordinals in Zermelo-Fraenkel Set Theory 
     6 Ordinals in Zermelo-Fraenkel Set Theory 
     7 *)
     7 *)
     8 
     8 
     9 Ordinal = WF + Bool + "simpdata" + "equalities" +
     9 Ordinal = WF + Bool + "simpdata" + "equalities" +
    10 consts
    10 consts
    11   Memrel      	:: "i=>i"
    11   Memrel      	:: i=>i
    12   Transset,Ord  :: "i=>o"
    12   Transset,Ord  :: i=>o
    13   "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
    13   "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
    14   "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
    14   "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
    15   Limit         :: "i=>o"
    15   Limit         :: i=>o
    16 
    16 
    17 translations
    17 translations
    18   "x le y"      == "x < succ(y)"
    18   "x le y"      == "x < succ(y)"
    19 
    19 
    20 defs
    20 defs