1signature Thm_cont =
2sig
3  include Abbrev
4
5  val THEN_TCL         : thm_tactical * thm_tactical -> thm_tactical
6  val ORELSE_TCL       : thm_tactical * thm_tactical -> thm_tactical
7  val REPEAT_TCL       : thm_tactical -> thm_tactical
8  val REPEAT_GTCL      : thm_tactical -> (thm -> tactic) -> thm_tactic
9  val ALL_THEN         : thm_tactical
10  val NO_THEN          : thm_tactical
11  val EVERY_TCL        : thm_tactical list -> thm_tactical
12  val FIRST_TCL        : thm_tactical list -> thm_tactical
13  val CONJUNCTS_THEN2  : thm_tactic -> thm_tactical
14  val CONJUNCTS_THEN   : thm_tactical
15  val DISJ_CASES_THEN2 : thm_tactic -> thm_tactical
16  val DISJ_CASES_THEN  : thm_tactical
17  val DISJ_CASES_THENL : thm_tactic list -> thm_tactic
18  val DISCH_THEN       : thm_tactic -> tactic
19  val disch_then       : thm_tactic -> tactic
20  val UNDISCH_THEN     : Term.term -> thm_tactic -> tactic
21  val X_CHOOSE_THEN    : Term.term -> thm_tactical
22  val CHOOSE_THEN      : thm_tactical
23  val X_CASES_THENL    : (('a list -> 'b list -> ('a * 'b) list)
24                          -> thm_tactic list -> (term list * thm_tactic) list)
25                            -> thm_tactic list -> thm_tactic
26  val X_CASES_THEN     : Term.term list list -> thm_tactical
27  val CASES_THENL      : thm_tactic list -> thm_tactic
28  val STRIP_THM_THEN   : thm_tactical
29
30  val ANTE_RES_THEN    : thm_tactical
31  val IMP_RES_THEN     : thm_tactic -> thm -> tactic
32  val RES_THEN         : thm_tactic -> tactic
33  val PROVEHYP_THEN    : (thm -> thm -> tactic) -> thm -> tactic
34  val provehyp_then    : (thm -> thm -> tactic) -> thm -> tactic
35end
36