src/ZF/Ordinal.thy
changeset 78370 fda3f7a158b9
parent 76216 9fc34f76b4e8
equal deleted inserted replaced
78369:ba71ea02d965 78370:fda3f7a158b9