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