src/ZF/CardinalArith.thy
changeset 30368 1a2a54f910c9
parent 27517 c055e1d49285
child 32960 69916a850301