equal
deleted
inserted
replaced
35 (*needed because jump_cardinal(K) might not be the successor of K*) |
35 (*needed because jump_cardinal(K) might not be the successor of K*) |
36 csucc :: "i=>i" |
36 csucc :: "i=>i" |
37 "csucc(K) == LEAST L. Card(L) & K<L" |
37 "csucc(K) == LEAST L. Card(L) & K<L" |
38 |
38 |
39 syntax (xsymbols) |
39 syntax (xsymbols) |
|
40 "op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65) |
|
41 "op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70) |
|
42 syntax (HTML output) |
40 "op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65) |
43 "op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65) |
41 "op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70) |
44 "op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70) |
42 |
45 |
43 |
46 |
44 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))" |
47 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))" |