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