1signature holyHammer =
2sig
3
4  include Abbrev
5  datatype prover = Eprover | Z3 | Vampire
6
7  val set_timeout : int -> unit
8  val dep_flag : bool ref (* remove limits on the number of premises *)
9  val holyhammer  : term -> thm
10  val hh          : tactic
11  (* For running holyhammer in the backgroup with a high time limit *)
12  val hh_fork     : goal -> Thread.thread
13  (* string list is a list of premises of the form "fooTheory.bar" *)
14  val hh_pb       : prover list -> string list -> goal -> tactic
15
16  (* Evaluation of holyhammer (without premise selection) *)
17  val hh_pb_eval_thm : prover list -> string * thm -> unit
18  val hh_pb_eval_thy : prover list -> string -> unit
19
20  (* Evaluation of holyhammer (with premise selection).
21     This function is used inside the tactictoe evaluation framework. *)
22  val hh_eval : mlThmData.thmdata * mlTacticData.tacdata -> goal -> unit
23
24end
25