start: ProofEngineTypes.tactic ->
continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+ (** "folding" of then_ *)
+val seq: tactics: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
val repeat_tactic:
tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
val solve_tactics:
tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
-
+val fail: ProofEngineTypes.tactic
(*
val prova_tac : ProofEngineTypes.tactic