val first: tactics: tactic list -> tactic
val thens: start: tactic -> continuations: tactic list -> tactic
val then_: start: tactic -> continuation: tactic -> tactic
+val ifs: start: tactic -> continuations: tactic list -> fail: tactic -> tactic
val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic
val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
val repeat_tactic: tactic: tactic -> tactic