[isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

[Tobias Nipkow]

Indeed, and that is consistent with informal language, eg "sorted by size". It 
looks like "wrt" is really better for relations.

Tobias

On 16/08/2017 17:04, Peter Lammich wrote:
> However, sort_by takes a function mapping the elements into a linear order, 
> which is less general than allowing arbitrary (preorder?) relations.
> 
> Peter
> 
> 
> -------- Original Message --------
> Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added 
> Data_Structures/Binomial_Heap.thy
> From: Makarius
> To: Tobias Nipkow ,isabelle-dev at mailbroy.informatik.tu-muenchen.de
> CC:
> 
> 
>     On 16/08/17 16:10, Tobias Nipkow wrote:
>      >
>      > Concerning "sorted_by" vs "sorted_wrt": the latter seems closer to
>      > informal usage. But if many people cry out for "by" we could change that.
> 
>     In Isabelle/ML we used to have "sort_wrt" for some decades, but I have
>     changed that recently into into "sort_by" to make it coincide with the
>     terminology of the Scala library.
> 
>     See
>     http://isabelle.in.tum.de/repos/isabelle/rev/610794dff23c
> 
> 
>     Makarius
>     _______________________________________________
>     isabelle-dev mailing list
>     isabelle-dev at in.tum.de
>     https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170816/58776a8c/attachment.bin>