src/ZF/ord.ML
changeset 5944 dcc446da8e19
parent 186 320f6bdb593a
equal deleted inserted replaced
5943:576a7f5e5e39 5944:dcc446da8e19