2012-07-16 | wenzelm | more direct Sorts.has_instance; | changeset | files |
2012-07-16 | wenzelm | replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort; | changeset | files |
Loading... |