[isabelle-dev] Merge-Sort Implementation

[Lawrence Paulson]

If my memory is correct, quicksort was the clear winner in the performance tests that I undertook for my book.
Larry

On 27 Oct 2011, at 13:50, Florian Haftmann wrote:

> interesting to read that comment.  The exiting quicksort implementation
> in HOL is indeed taken from Isabelle's ML library.  Don't know what the
> ancient motivation for quicksort has been (maybe others can comment on
> this).