src/HOL/Tools/function_package/lexicographic_order.ML
changeset 30787 5b7a5a05c7aa
parent 30715 e23e15f52d42