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). _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev