src/HOL/Tools/Function/lexicographic_order.ML
changeset 35757 c2884bec5463
parent 35402 115a5a95710a
child 36521 73ed9f18fdd3