src/ZF/CardinalArith.thy
changeset 40822 98a5faa5aec0
parent 39159 0dec18004e75
child 45602 2a858377c3d2