src/HOL/Tools/Function/lexicographic_order.ML
changeset 44262 355d5438f5fb
parent 42795 66fcc9882784
child 45740 132a3e1c0fe5