src/ZF/OrderType.thy
changeset 39220 8420a873f534
parent 32960 69916a850301
child 46820 c656222c4dc1