changeset 61394 | 6142b282b164 |
parent 61378 | 3e04c9ca001a |
child 61401 | 4d9c716e7786 |
--- a/src/ZF/CardinalArith.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/CardinalArith.thy Sat Oct 10 22:14:44 2015 +0200 @@ -37,7 +37,7 @@ csucc :: "i=>i" where --\<open>needed because @{term "jump_cardinal(K)"} might not be the successor of @{term K}\<close> - "csucc(K) == LEAST L. Card(L) & K<L" + "csucc(K) == \<mu> L. Card(L) & K<L" notation (xsymbols) cadd (infixl "\<oplus>" 65) and