1signature jrhTactics =
2  sig
3    include Abbrev
4    type Goal         = thm list * term
5    type Goalstate    = Goal list * validation
6    type Tactic       = Goal -> Goalstate
7    type Thm_Tactic   = thm -> Tactic
8    type Thm_Tactical = Thm_Tactic -> Thm_Tactic
9    type refinement   = Goalstate -> Goalstate
10
11    val by  : Tactic -> refinement
12    val bys : Tactic list -> refinement
13    val rotate : int -> refinement
14
15    val mk_Goalstate : Goal -> Goalstate
16
17    val THEN    : Tactic * Tactic -> Tactic
18    val ORELSE  : Tactic * Tactic -> Tactic
19    val THENL   : Tactic * Tactic list -> Tactic
20    val convert : Tactic -> tactic
21
22    (* some actual tactics *)
23    val ALL_TAC        : Tactic
24    val ACCEPT_TAC     : Thm_Tactic
25    val ASSUME_TAC     : Thm_Tactic
26    val CONTR_TAC      : Thm_Tactic
27    val DISJ_CASES_TAC : Thm_Tactic
28    val POP_ASSUM      : Thm_Tactic -> Tactic
29    val POP_ASSUM_LIST : (thm list -> Tactic) -> Tactic
30    val FIRST_ASSUM    : Thm_Tactic -> Tactic
31    val ASSUM_LIST     : (thm list -> Tactic) -> Tactic
32    val RULE_ASSUM_TAC : (thm -> thm) -> Tactic
33
34    val REPEAT         : Tactic -> Tactic
35    val EVERY          : Tactic list -> Tactic
36    val MAP_EVERY      : ('a -> Tactic) -> 'a list -> Tactic
37    val CHOOSE_TAC     : Thm_Tactic
38    val FIRST_X_ASSUM  : Thm_Tactic -> Tactic
39
40    (* some theorem tacticals *)
41
42    val CONJUNCTS_THEN  : Thm_Tactical
43    val DISJ_CASES_THEN : Thm_Tactical
44    val ORELSE_TCL      : Thm_Tactical * Thm_Tactical -> Thm_Tactical
45end
46