src/HOL/Tools/Function/lexicographic_order.ML
changeset 45693 bbd2c7ffc02c
parent 42795 66fcc9882784
child 45740 132a3e1c0fe5