src/ZF/Ordinal.thy
changeset 2539 ddd22ceee8cc
parent 2469 b50b8c0eec01
child 2540 ba8311047f18
     1.1 --- a/src/ZF/Ordinal.thy	Thu Jan 23 10:35:28 1997 +0100
     1.2 +++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:40:21 1997 +0100
     1.3 @@ -11,8 +11,10 @@
     1.4    Memrel        :: i=>i
     1.5    Transset,Ord  :: i=>o
     1.6    "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
     1.7 +  Limit         :: i=>o
     1.8 +
     1.9 +syntax
    1.10    "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
    1.11 -  Limit         :: i=>o
    1.12  
    1.13  translations
    1.14    "x le y"      == "x < succ(y)"