src/ZF/CardinalArith.thy
changeset 12114 a8e860c86252
parent 9964 7966a2902266
child 12667 7e6eaaa125f2
     1.1 --- a/src/ZF/CardinalArith.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4    (*needed because jump_cardinal(K) might not be the successor of K*)
     1.5    csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "op |+|"     :: [i,i] => i          (infixl "\\<oplus>" 65)
    1.10    "op |*|"     :: [i,i] => i          (infixl "\\<otimes>" 70)
    1.11