src/ZF/Ordinal.thy
changeset 78585 cf114894a5ed
parent 76216 9fc34f76b4e8