src/HOL/Tools/Function/lexicographic_order.ML
changeset 47247 23654b331d5c
parent 45740 132a3e1c0fe5
child 47432 e1576d13e933