src/ZF/CardinalArith.thy
changeset 45379 0147a4348ca1
parent 39159 0dec18004e75
child 45602 2a858377c3d2