src/HOL/Tools/Function/lexicographic_order.ML
changeset 34968 ceeffca32eb0
parent 34232 36a2a3029fd3
child 34974 18b41bba42b5
equal deleted inserted replaced
34966:52f30b06938a 34968:ceeffca32eb0