src/HOL/Tools/function_package/lexicographic_order.ML
changeset 24930 cc2e0e8c81af
parent 24920 2a45e400fdad
child 24961 5298ee9c3fe5