src/ZF/Ordinal.thy
changeset 22207 4bc4a930a8bc
parent 16417 9bc16273c2d4
child 22808 a7daa74e2980
equal deleted inserted replaced
22206:8cc04341de38 22207:4bc4a930a8bc