equal
deleted
inserted
replaced
37 UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" |
37 UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" |
38 |
38 |
39 (*needed because jump_cardinal(K) might not be the successor of K*) |
39 (*needed because jump_cardinal(K) might not be the successor of K*) |
40 csucc_def "csucc(K) == LEAST L. Card(L) & K<L" |
40 csucc_def "csucc(K) == LEAST L. Card(L) & K<L" |
41 |
41 |
42 syntax (symbols) |
42 syntax (xsymbols) |
43 "op |*|" :: [i,i] => i (infixr "|\\<times>|" 70) |
43 "op |+|" :: [i,i] => i (infixl "\\<oplus>" 65) |
|
44 "op |*|" :: [i,i] => i (infixl "\\<otimes>" 70) |
44 |
45 |
45 end |
46 end |