src/ZF/Arith.thy

--- a/src/ZF/Arith.thy	Fri Sep 15 00:17:51 2000 +0200
+++ b/src/ZF/Arith.thy	Fri Sep 15 00:18:36 2000 +0200
@@ -56,7 +56,10 @@
   mod  :: [i,i]=>i                    (infixl "mod" 70)
     "m mod n == raw_mod (natify(m), natify(n))"
 
-syntax (xsymbols)
+syntax (symbols)
+  "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
+
+syntax (HTML output)
   "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
 
 end