diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/CardinalArith.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,9 @@
 syntax (xsymbols)
   "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
   "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
+syntax (HTML output)
+  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
+  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
 
 
 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"