val mk_tactic : (input_status -> output_status) -> tactic
val apply_tactic : tactic -> input_status -> output_status
val goals : output_status -> goal list * goal list (** opened, closed goals *)
val mk_tactic : (input_status -> output_status) -> tactic
val apply_tactic : tactic -> input_status -> output_status
val goals : output_status -> goal list * goal list (** opened, closed goals *)