HOL-ex.Sorting_Algorithms_Examples