1signature tuerk_tacticsLib = 2sig 3 4 val FORALL_EQ_STRIP_TAC : Abbrev.tactic 5 val EXISTS_EQ_STRIP_TAC : Abbrev.tactic 6 val CLEAN_ASSUMPTIONS_TAC : Abbrev.tactic 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 13 val DISJ_EQ_STRIP_TAC : Abbrev.tactic 14 val CONJ_EQ_STRIP_TAC : Abbrev.tactic 15 val A_IMP_EQ_STRIP_TAC : Abbrev.tactic 16 val C_IMP_EQ_STRIP_TAC : Abbrev.tactic 17 val BOOL_EQ_STRIP_TAC : Abbrev.tactic 18 19 val WEAKEN_HD_TAC : Abbrev.tactic 20 val IMP_TAC : Abbrev.thm -> Abbrev.tactic 21 val SET_INDUCT_TAC : Abbrev.tactic 22 val GSYM_NO_TAC : int -> Abbrev.tactic 23 val WEAKEN_NO_TAC : int -> Abbrev.tactic 24 25 val SUBGOAL_TAC : Abbrev.term frag list -> Abbrev.tactic 26 val REMAINS_TAC : Abbrev.term frag list -> Abbrev.tactic 27 val SPEC_NO_ASSUM : int -> Abbrev.term -> 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 31 32 val UNDISCH_HD_TAC : Abbrev.tactic 33 val UNDISCH_ALL_TAC : Abbrev.tactic 34 val UNDISCH_NO_TAC : int -> Abbrev.tactic 35 val UNDISCH_KEEP_NO_TAC: int -> Abbrev.tactic 36 val POP_NO_ASSUM : int -> (Abbrev.thm -> Abbrev.tactic) -> Abbrev.tactic 37 val LEFT_DISJ_TAC : Abbrev.tactic 38 val RIGHT_DISJ_TAC : Abbrev.tactic 39 val LEFT_CONJ_TAC : Abbrev.tactic 40 val RIGHT_CONJ_TAC : Abbrev.tactic 41 val IMP_TO_EQ_TAC : Abbrev.tactic 42 43 val EXISTS_LEAST_TAC___GEN : Abbrev.term -> Abbrev.tactic -> Abbrev.tactic; 44 val EXISTS_LEAST_TAC : Abbrev.term -> Abbrev.tactic; 45 val Q_EXISTS_LEAST_TAC : Abbrev.term frag list -> Abbrev.tactic; 46 47 48 val PROVE_CONDITION_TAC : (Abbrev.thm -> Abbrev.tactic) 49 val PROVE_CONDITION_NO_ASSUM : int -> Abbrev.tactic 50 51 val MATCH_LEFT_EQ_MP_TAC : Abbrev.thm -> Abbrev.tactic; 52 val MATCH_RIGHT_EQ_MP_TAC : Abbrev.thm -> Abbrev.tactic; 53 54 val store_simp_thm: (string * Abbrev.term * Abbrev.tactic) -> Abbrev.thm 55end 56 57