src/HOL/Tools/Function/lexicographic_order.ML
changeset 42497 89acb654d8eb
parent 42361 23f352990944
child 42774 6c999448c2bb