src/ZF/CardinalArith.thy
changeset 80408 e6d3d1db6136
parent 76217 8655344f1cf6