src/ZF/Ordinal.thy
changeset 80517 720849fb1f37
parent 76216 9fc34f76b4e8