src/ZF/CardinalArith.thy
changeset 80417 10ab5a74f6f5
parent 76217 8655344f1cf6