src/ZF/CardinalArith.thy
changeset 1160 8845eb5f0e5e
parent 1155 928a16e02f9f
child 1401 0c439768f45c