1signature combinSyntax =
2sig
3  include Abbrev
4
5  val K_tm      : term
6  val S_tm      : term
7  val I_tm      : term
8  val C_tm      : term
9  val W_tm      : term
10  val o_tm      : term
11  val update_tm : term
12  val fail_tm   : term
13
14  val mk_K      : term * term -> term
15  val mk_K_1    : term * hol_type -> term
16  val mk_S      : term * term * term -> term
17  val mk_I      : term -> term
18  val mk_C      : term * term * term -> term
19  val mk_W      : term * term -> term
20  val mk_o      : term * term -> term
21  val mk_update : term * term -> term
22  val mk_fail   : term * string * term list -> term
23
24  val dest_K           : term -> term * term
25  val dest_K_1         : term -> term
26  val dest_S           : term -> term * term * term
27  val dest_I           : term -> term
28  val dest_C           : term -> term * term * term
29  val dest_W           : term -> term * term
30  val dest_o           : term -> term * term
31  val dest_update      : term -> term * term
32  val dest_update_comb : term -> (term * term) * term
33  val strip_update     : term -> (term * term) list * term
34  val dest_fail        : term -> term * string * term list
35
36  val is_K           : term -> bool
37  val is_K_1         : term -> bool
38  val is_S           : term -> bool
39  val is_I           : term -> bool
40  val is_C           : term -> bool
41  val is_W           : term -> bool
42  val is_o           : term -> bool
43  val is_update      : term -> bool
44  val is_update_comb : term -> bool
45  val is_fail        : term -> bool
46
47end
48