src/ZF/Cardinal.thy
changeset 11990 c1daefc08eff
parent 9683 f87c8c449018
child 12861 7ec4807b53cf