src/ZF/Ordinal.thy

--- a/src/ZF/Ordinal.thy	Thu Jan 23 10:35:28 1997 +0100
+++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:40:21 1997 +0100
@@ -11,8 +11,10 @@
   Memrel        :: i=>i
   Transset,Ord  :: i=>o
   "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
+  Limit         :: i=>o
+
+syntax
   "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
-  Limit         :: i=>o
 
 translations
   "x le y"      == "x < succ(y)"