Lines Matching refs:list
16 val THENL : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
17 val >| : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic
19 val THENL : tactic * tactic list -> tactic
20 val THENL : list_tactic * tactic list -> list_tactic
34 val TACS_TO_LT : tactic list -> list_tactic
64 val ADD_SGS_TAC : term list -> tactic -> tactic
65 val EVERY : tactic list -> tactic
66 val EVERY_LT : list_tactic list -> list_tactic
67 val FIRST : tactic list -> tactic
68 val MAP_EVERY : ('a -> tactic) -> 'a list -> tactic
69 val map_every : ('a -> tactic) -> 'a list -> tactic
70 val MAP_FIRST : ('a -> tactic) -> 'a list -> tactic
71 val FIRST_PROVE : tactic list -> tactic
85 val ASSUM_LIST : (thm list -> tactic) -> tactic
91 val POP_ASSUM_LIST : (thm list -> tactic) -> tactic
95 val Q_TAC0 : {traces : (string * int) list} -> hol_type option ->