src/ZF/Ordinal.thy
changeset 1401 0c439768f45c
parent 852 664052e3cf66
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Ordinal.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Ordinal.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  Ordinal = WF + Bool + "simpdata" + "equalities" +
     1.6  consts
     1.7 -  Memrel      	:: "i=>i"
     1.8 -  Transset,Ord  :: "i=>o"
     1.9 -  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
    1.10 -  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
    1.11 -  Limit         :: "i=>o"
    1.12 +  Memrel      	:: i=>i
    1.13 +  Transset,Ord  :: i=>o
    1.14 +  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
    1.15 +  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
    1.16 +  Limit         :: i=>o
    1.17  
    1.18  translations
    1.19    "x le y"      == "x < succ(y)"