Lines Matching refs:list
14 type ('a,'b)hol88subst = ('b * 'a) list
16 val match : term -> term -> (term * term) list * (hol_type * hol_type) list
17 val assoc : ''a -> (''a * 'b) list -> ''a * 'b
18 val rev_assoc : ''a -> ('b * ''a) list -> 'b * ''a
19 val frees : term -> term list
21 val GEN_REWRITE_RULE : (conv -> conv) -> thm list -> thm list -> thm -> thm
22 val GEN_REWRITE_TAC : (conv -> conv) -> thm list -> thm list -> tactic
23 val variant : term list -> term -> term
27 substitution is a list of pairs