# HG changeset patch
# User wenzelm
# Date 968969916 -7200
# Node ID 7966a29022666b9b43cf7c5561a5e9bf0a45f369
# Parent  6342d9c7fe46b9b8d5d98ffac16bee1fe0b5f0a6
tuned symbols;

diff -r 6342d9c7fe46 -r 7966a2902266 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
diff -r 6342d9c7fe46 -r 7966a2902266 src/ZF/CardinalArith.thy
--- 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)
 
diff -r 6342d9c7fe46 -r 7966a2902266 src/ZF/Integ/Int.thy
--- 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
diff -r 6342d9c7fe46 -r 7966a2902266 src/ZF/OrderType.thy
--- 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