src/HOL/Tools/function_package/lexicographic_order.ML
changeset 23303 6091e530ff77
parent 23128 8e0abe0fa80f
child 23437 4a44fcc9dba9