src/ZF/Ordinal.thy
changeset 852 664052e3cf66
parent 753 ec86863e87c8
child 1401 0c439768f45c
equal deleted inserted replaced
851:f9172c4625f1 852:664052e3cf66
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 Ordinals in Zermelo-Fraenkel Set Theory 
     6 Ordinals in Zermelo-Fraenkel Set Theory 
     7 *)
     7 *)
     8 
     8 
     9 Ordinal = WF + "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*)