Lines Matching refs:list
31 val print_terms : term list -> unit
33 val print_theorems : thm list -> unit
34 val print_goal : (term list * term) -> unit
100 : thm -> term -> (term * term) list * (hol_type * hol_type) list
102 : thm -> term -> (term * term) list * (hol_type * hol_type) list
106 : thm -> term -> (term * term) list * (hol_type * hol_type) list
108 : thm -> term -> (term * term) list * (hol_type * hol_type) list
127 val REWRITE_ASSUM_TAC : thm list -> tactic
128 val REWRITE_ALL_TAC : thm list -> tactic
129 val ASM_REWRITE_ALL_TAC : thm list -> tactic
130 val ONCE_REWRITE_ASSUM_TAC : thm list -> tactic
131 val ONCE_REWRITE_ALL_TAC : thm list -> tactic
132 val ONCE_ASM_REWRITE_ALL_TAC : thm list -> tactic
141 val EVERY1 : tactic list -> tactic