src/ZF/CardinalArith.thy
changeset 15827 5fdf2d8dab9c
parent 14883 ca000a495448
child 16417 9bc16273c2d4