However, sort_by takes a function mapping the elements into a linear order, which is less general than allowing arbitrary (preorder?) relations.<br><br>Peter<div class="quote" style="line-height: 1.5"><br><br>-------- Original Message --------<br>Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy<br>From: Makarius <makarius@sketis.net><br>To: Tobias Nipkow <nipkow@in.tum.de>,isabelle-dev@mailbroy.informatik.tu-muenchen.de<br>CC: <br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 16/08/17 16:10, Tobias Nipkow wrote:<br>> <br>> Concerning "sorted_by" vs "sorted_wrt": the latter seems closer to<br>> informal usage. But if many people cry out for "by" we could change that.<br><br>In Isabelle/ML we used to have "sort_wrt" for some decades, but I have<br>changed that recently into into "sort_by" to make it coincide with the<br>terminology of the Scala library.<br><br>See<br>http://isabelle.in.tum.de/repos/isabelle/rev/610794dff23c<br><br><br>       Makarius<br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br></blockquote></div>