src/HOL/Tools/Function/lexicographic_order.ML
changeset 55407 81f7e60755c3
parent 51958 bca32217b304
child 56231 b98813774a63