1.1 --- a/src/ZF/CardinalArith.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -39,6 +39,9 @@
     1.4  syntax (xsymbols)
     1.5    "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
     1.6    "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
     1.7 +syntax (HTML output)
     1.8 +  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
     1.9 +  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
    1.10  
    1.11  
    1.12  lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"