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