src/ZF/Ordinal.thy
changeset 524 b1bf18e83302
parent 435 ca5356bd315a
child 753 ec86863e87c8