src/ZF/CardinalArith.thy
changeset 38340 7813e44db886
parent 32960 69916a850301
child 39159 0dec18004e75