src/HOL/Tools/function_package/lexicographic_order.ML
changeset 23303 6091e530ff77
parent 23128 8e0abe0fa80f
child 23437 4a44fcc9dba9
equal deleted inserted replaced
23302:919d5c1fe509 23303:6091e530ff77