src/HOL/Tools/Function/lexicographic_order.ML
changeset 46631 2c5c003cee35
parent 45740 132a3e1c0fe5
child 47432 e1576d13e933