Lines Matching refs:list
10 val ASM_LIST_TAC : int list
11 -> (thm list -> term list * 'a -> 'b)
12 -> term list * 'a -> 'b
13 val ASM_TAC : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b
32 val MP2_TAC : thm -> goal -> (term list * term) list * (thm list -> thm)
33 val MY_MP_TAC : term -> goal -> (term list * term) list * (thm list -> thm)
34 val POP_NO_ASSUM : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b
51 val delete : int -> 'a list -> 'a list
52 val elem : int -> 'a list -> 'a