src/ZF/OrderType.thy
changeset 578 efc648d29dd0
parent 467 92868dab2939
child 753 ec86863e87c8