src/HOL/Tools/function_package/lexicographic_order.ML
changeset 21212 547224bf9348
parent 21201 803bc7672d17
child 21237 b803f9870e97