src/HOL/Tools/Function/lexicographic_order.ML
changeset 46218 ecf6375e2abb
parent 45740 132a3e1c0fe5
child 47432 e1576d13e933
equal deleted inserted replaced
46217:7b19666f0e3d 46218:ecf6375e2abb