src/HOL/Tools/Function/lexicographic_order.ML
changeset 55767 96ddf9bf12ac
parent 51958 bca32217b304
child 56231 b98813774a63