src/ZF/Cardinal.thy
changeset 14598 7009f59711e3
parent 14565 c6dc17aab88a
child 14883 ca000a495448