src/ZF/CardinalArith.thy
changeset 80176 7fefa7839ac6
parent 76217 8655344f1cf6