src/ZF/Ordinal.thy
changeset 12114 a8e860c86252
parent 2540 ba8311047f18
child 13155 dcbf6cb95534
     1.1 --- a/src/ZF/Ordinal.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/ZF/Ordinal.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  translations
     1.5    "x le y"      == "x < succ(y)"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
    1.10  
    1.11  defs