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