src/ZF/Ordinal.thy
changeset 13465 08e3fe248ba9
parent 13396 11219ca224ab
child 13534 ca6debb89d77