Mon, 16 Jul 2012 21:20:56 +0200 | wenzelm | more direct Sorts.has_instance; | changeset | files |
Mon, 16 Jul 2012 15:57:21 +0200 | wenzelm | replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort; | changeset | files |