src/ZF/CardinalArith.thy
changeset 79060 9f2040e5e2d6
parent 76217 8655344f1cf6