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