src/ZF/CardinalArith.thy
changeset 45397 20128348e9b9
parent 39159 0dec18004e75
child 45602 2a858377c3d2