src/HOL/Tools/Function/lexicographic_order.ML
changeset 82733 8b537e1af2ec
parent 82590 d08f5b5ead0a