src/ZF/OrderType.thy
changeset 81418 de8dbdadda76
parent 76217 8655344f1cf6