[isabelle-dev] Merge-Sort Implementation

Lawrence Paulson lp15 at cam.ac.uk
Thu Oct 27 15:36:14 CEST 2011

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

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).

More information about the isabelle-dev mailing list