src/ZF/Ordinal.thy
changeset 13509 6f168374652a
parent 13396 11219ca224ab
child 13534 ca6debb89d77