1signature sortingSyntax = 2sig 3 4 include Abbrev 5 6 val part3_tm: term 7 val part_tm: term 8 val partition_tm: term 9 val perm_tm: term 10 val qsort3_tm: term 11 val qsort_tm: term 12 val sorted_tm: term 13 14 val dest_part: term -> term * term * term * term 15 val dest_part3: term -> term * term * term 16 val dest_partition: term -> term * term 17 val dest_perm: term -> term * term 18 val dest_qsort: term -> term * term 19 val dest_qsort3: term -> term * term 20 val dest_sorted: term -> term * term 21 22 val is_part: term -> bool 23 val is_part3: term -> bool 24 val is_partition: term -> bool 25 val is_perm: term -> bool 26 val is_qsort: term -> bool 27 val is_qsort3: term -> bool 28 val is_sorted: term -> bool 29 30 val mk_part: term * term * term * term -> term 31 val mk_part3: term * term * term -> term 32 val mk_partition: term * term -> term 33 val mk_perm: term * term -> term 34 val mk_qsort: term * term -> term 35 val mk_qsort3: term * term -> term 36 val mk_sorted: term * term -> term 37end 38