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