1structure sortingLib :> sortingLib =
2struct
3
4  open computeLib sortingTheory
5
6  val add_sorting_compset =
7      extend_compset [
8        Defs [
9          PARTITION_DEF, PART_DEF, QSORT_DEF
10        ]
11      ]
12
13end
14