src/HOL/Tools/Function/lexicographic_order.ML
changeset 52088 7d8b53e80ce7
parent 51958 bca32217b304
child 56231 b98813774a63