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 prova_tac : ProofEngineTypes.tactic
-*)
+val fail_tac: ProofEngineTypes.tactic