Lines Matching refs:list
7 val REWRITE_ASSUMPTIONS_TAC : Abbrev.thm list -> Abbrev.tactic
8 val REWRITE_ALL_TAC : Abbrev.thm list -> Abbrev.tactic
9 val ONCE_REWRITE_ASSUMPTIONS_TAC : Abbrev.thm list -> Abbrev.tactic
10 val ONCE_REWRITE_ALL_TAC : Abbrev.thm list -> Abbrev.tactic
11 val SIMP_ASSUMPTIONS_TAC : simpLib.simpset -> Abbrev.thm list -> Abbrev.tactic
12 val SIMP_ALL_TAC : simpLib.simpset -> Abbrev.thm list -> Abbrev.tactic
25 val SUBGOAL_TAC : Abbrev.term frag list -> Abbrev.tactic
26 val REMAINS_TAC : Abbrev.term frag list -> Abbrev.tactic
28 val SPECL_NO_ASSUM : int -> Abbrev.term list -> Abbrev.tactic
29 val Q_SPEC_NO_ASSUM : int -> Abbrev.term frag list -> Abbrev.tactic
30 val Q_SPECL_NO_ASSUM : int -> Abbrev.term frag list list -> Abbrev.tactic
45 val Q_EXISTS_LEAST_TAC : Abbrev.term frag list -> Abbrev.tactic;