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