src/HOL/Tools/Function/lexicographic_order.ML
changeset 33020 0908ed080ccf
parent 32952 aeb1e44fbc19
child 33099 b8cdd3d73022