--- a/src/ZF/Arith.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Arith.thy Thu Aug 24 11:05:20 2000 +0200
@@ -56,7 +56,7 @@
mod :: [i,i]=>i (infixl "mod" 70)
"m mod n == raw_mod (natify(m), natify(n))"
-syntax (symbols)
+syntax (xsymbols)
"mult" :: [i, i] => i (infixr "#\\<times>" 70)
end