Lines Matching refs:list
21 val list_mk_union : term list -> term
29 val list_mk_insert : term list * term -> term
32 val strip_union : term -> term list
50 val mk_bag : term list * hol_type -> term
51 val strip_insert : term -> term list * term
52 val dest_bag : term -> term list * hol_type
59 val SBAG_SOLVE : thm list -> term -> thm
62 val BAG_RESORT_CONV : int list -> conv
64 val GET_BAG_IN_THMS : term -> thm list
68 val get_resort_list___pred : (term -> bool) -> term -> int list
70 val get_resort_lists___pred_pair : (term -> term -> bool) -> term -> term -> (int list * int list)