src/HOL/Tools/Function/lexicographic_order.ML
changeset 42224 578a51fae383
parent 41540 414a68d72279
child 42361 23f352990944