--- a/src/ZF/Ordinal.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/Ordinal.thy Fri Nov 09 00:09:47 2001 +0100
@@ -19,7 +19,7 @@
translations
"x le y" == "x < succ(y)"
-syntax (symbols)
+syntax (xsymbols)
"op le" :: [i,i] => o (infixl "\\<le>" 50) (*less than or equals*)
defs