src/ZF/OrderType.thy
changeset 68147 a8f40dd73c61
parent 63648 f9f3006a5579
child 68490 eb53f944c8cd