text_raw‹\section*{Sorting a list by two keys}› theory Linorder_Helper imports Main begin text‹Sorting is fun...› text‹The problem is that Isabelle does not have anything like \texttt{sortBy}, only @{const sort_key}. This means that there is no way to sort something based on two properties, with one being infinitely more important.› text‹Enter this:›