src/HOL/Tools/Function/lexicographic_order.ML
changeset 52389 3971dd9ca831
parent 51958 bca32217b304
child 56231 b98813774a63