src/ZF/CardinalArith.thy
changeset 45107 76fef3e57004
parent 39159 0dec18004e75
child 45602 2a858377c3d2