src/ZF/AC/Cardinal_aux.thy
changeset 45107 76fef3e57004
parent 36319 8feb2c4bef1a
child 46822 95f1e700b712