1signature wfrecUtils = 2sig 3 include Abbrev 4 5 val zip3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list 6 val unzip3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list 7 val gtake : ('a -> 'b) -> int * 'a list -> 'b list * 'a list 8 val list_to_string : ('a -> string) -> string -> 'a list -> string 9 10 val mk_sum_type : hol_type -> hol_type -> hol_type 11 val mk_prod_type : hol_type -> hol_type -> hol_type 12 val list_mk_fun_type : hol_type list -> hol_type 13 val list_mk_prod_type : hol_type list -> hol_type 14 val strip_fun_type : hol_type -> hol_type list * hol_type 15 val strip_prod_type : hol_type -> hol_type list 16 17 val atom_name : term -> string 18 val mk_vstruct : hol_type -> term list -> term * term list 19 val gen_all : term -> term 20 val strip_imp : term -> term list * term 21 val dest_relation : term -> term * term * term 22 val is_WFR : term -> bool 23 val func_of_cond_eqn : term -> term 24 val vary : term list -> hol_type -> term 25 val match_type : 'a -> hol_type -> hol_type -> (hol_type,hol_type)subst 26 val match_term : 'a -> term -> term 27 -> (term,term) subst * (hol_type,hol_type) subst 28 29end 30