Lines Matching refs:list
21 val RW : thm list -> rule
22 val RW1 : thm list -> rule
30 val quote_to_strings : 'a quotation -> string list
34 val all_distinct : ''a list -> ''a list
36 val collect_term_of_type : hol_type -> term -> term list
37 val find_terml : (term -> bool) -> term -> term list
38 val find_terml_all : (term -> bool) -> term -> term list
43 val list_dest : ('a -> 'a * 'a) -> 'a -> 'a list
44 val list_mk : (term * term -> term) -> term list -> term -> term
58 val list_mk_star : term list -> hol_type -> term
59 val word_patterns : term list
68 val EVAL_ANY_MATCH_CONV : term list -> conv
72 val GEN_MOVE_OUT_CONV : (term list -> term list) -> conv
73 val LIST_MOVE_OUT_CONV : bool -> term list -> conv
74 val MATCH_MOVE_OUT_CONV : term list -> conv
92 val EXISTS_PRE : term frag list -> rule
99 val LIST_HIDE_POST_RULE : term list -> rule
106 val SEP_REWRITE_RULE : thm list -> rule
107 val SUBST_INST : {redex: term, residue: term} list -> rule
111 val LIST_HIDE_SEP_IMP_POST_RULE : term list -> rule
119 val SPECL_FRAME_RULE : term list -> rule
120 val SPEC_COMPOSE_RULE : thm list -> thm
123 val SPEC_PROVE_TAC : thm list -> tactic
136 val SEP_S_TAC : string list -> thm -> tactic