src/ZF/OrderType.thy
changeset 9913 b9ecbe4667d0
parent 9683 f87c8c449018
child 9964 7966a2902266