src/HOL/Tools/Function/lexicographic_order.ML
changeset 33726 0878aecbf119
parent 33398 daa526c9e5d2
child 33855 cd8acf137c9c