src/ZF/AC/Cardinal_aux.thy
changeset 47496 a43f207f216f
parent 47101 ded5cc757bc9
child 60770 240563fbf41d