src/ZF/OrderType.ML
changeset 11982 65e2822d83dd
parent 9907 473a6604da94
child 12667 7e6eaaa125f2
equal deleted inserted replaced
11981:ad67e8d2c75f 11982:65e2822d83dd