Lines Matching refs:list
12 val free_vars : term -> term list
13 val free_vars_lr : term -> term list
14 val FVL : term list -> term set -> term set
16 val all_vars : term -> term list
18 val all_atomsl : term list -> term set -> term set
19 val free_varsl : term list -> term list
20 val all_varsl : term list -> term list
21 val type_vars_in_term : term -> hol_type list
25 val genvars : hol_type -> int -> term list
26 val variant : term list -> term -> term
27 val prim_variant : term list -> term -> term
28 val gen_variant : (string -> bool) -> string -> term list -> term -> term
32 val decls : string -> term list
33 val all_consts : unit -> term list
37 val list_mk_comb : term * term list -> term
40 val list_mk_binder : term option -> term list * term -> term
41 val list_mk_abs : term list * term -> term
46 val strip_binder : term option -> term -> term list * term
47 val strip_abs : term -> term list * term
67 val raw_match : hol_type list -> term set
71 ((hol_type,hol_type)subst * hol_type list)
72 val match_terml : hol_type list -> term set -> term -> term
76 ((hol_type,hol_type)subst * hol_type list)
92 val thy_consts : string -> term list