Lines Matching refs:list
5 type selection_fun = term -> (term -> int) -> term -> (term * string) list
11 val QUANT_ABBREV_CONV : selection_fun list -> quantHeuristicsLibBase.quant_param list -> conv
12 val QUANT_ABBREV_TAC : selection_fun list -> quantHeuristicsLibBase.quant_param list -> tactic
15 val SIMPLE_QUANT_ABBREV_CONV : selection_fun list -> conv
16 val SIMPLE_QUANT_ABBREV_TAC : selection_fun list -> tactic
20 val select_funs_combine : selection_fun list -> selection_fun
31 val select_fun_match_occ : int -> term frag list -> (term -> string) -> selection_fun
32 val select_fun_match : term frag list -> string -> selection_fun
33 val select_fun_pattern_occ : int -> term frag list -> selection_fun
34 val select_fun_pattern : term frag list -> selection_fun