src/HOL/Tools/Function/lexicographic_order.ML
changeset 46764 a65e18ceb1e3
parent 45740 132a3e1c0fe5
child 47432 e1576d13e933