val id_tac : ProofEngineTypes.tactic
-
-
- (* pseudo tacticals *)
+ (* tacticals *)
val try_tactics:
tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
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