src/HOL/Tools/Function/lexicographic_order.ML
changeset 58836 4037bb00d08e
parent 58819 aa43c6f05bca
child 59159 9312710451f5