--- 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
--- a/src/ZF/CardinalArith.thy Fri Sep 15 00:17:51 2000 +0200
+++ b/src/ZF/CardinalArith.thy Fri Sep 15 00:18:36 2000 +0200
@@ -39,7 +39,7 @@
(*needed because jump_cardinal(K) might not be the successor of K*)
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
-syntax (xsymbols)
+syntax (symbols)
"op |+|" :: [i,i] => i (infixl "\\<oplus>" 65)
"op |*|" :: [i,i] => i (infixl "\\<otimes>" 70)
--- a/src/ZF/Integ/Int.thy Fri Sep 15 00:17:51 2000 +0200
+++ b/src/ZF/Integ/Int.thy Fri Sep 15 00:18:36 2000 +0200
@@ -80,4 +80,7 @@
"zmult" :: [i,i] => i (infixr "$\\<times>" 70)
"zle" :: [i,i] => o (infixl "$\\<le>" 50) (*less than or equals*)
+syntax (HTML output)
+ "zmult" :: [i,i] => i (infixr "$\\<times>" 70)
+
end
--- a/src/ZF/OrderType.thy Fri Sep 15 00:17:51 2000 +0200
+++ b/src/ZF/OrderType.thy Fri Sep 15 00:18:36 2000 +0200
@@ -38,7 +38,10 @@
(*ordinal subtraction*)
odiff_def "i -- j == ordertype(i-j, Memrel(i))"
-syntax (xsymbols)
+syntax (symbols)
+ "op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
+
+syntax (HTML output)
"op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
end