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