* http://cs.unibo.it/helm/.
*)
+
+val id_tac : ProofEngineTypes.tactic
+
+
+
(* pseudo tacticals *)
val try_tactics:
tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+
val thens:
start: ProofEngineTypes.tactic ->
continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+
val then_:
start: ProofEngineTypes.tactic ->
continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+
+val repeat_tactic:
+ tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+val do_tactic:
+ n: int ->
+ tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+val try_tactic:
+ tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+val solve_tactics:
+ tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+
+
+
+(*
+val prova_tac : ProofEngineTypes.tactic
+*)