src/ZF/Ord.ML
changeset 12106 4a8558dbb6a0
parent 186 320f6bdb593a