src/ZF/OrderType.thy
changeset 77028 f5896dea6fce
parent 76217 8655344f1cf6