src/ZF/OrderType.thy
changeset 62337 d3996d5873dd
parent 61399 808222c1cf66
child 63168 466177e5736c