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