src/HOL/Tools/function_package/lexicographic_order.ML
changeset 27249 f339dc43ce9f
parent 26875 e18574413bc4
child 27330 1af2598b5f7d