src/ZF/CardinalArith.thy
changeset 78770 8a7c0f8fc9d2
parent 76217 8655344f1cf6