1signature hhReconstruct = 2sig 3 4 include Abbrev 5 6 (* Settings *) 7 val reconstruct_flag : bool ref 8 val minimization_timeout : real ref 9 val reconstruction_timeout : real ref 10 11 (* Read output of ATP *) 12 val get_lemmas : (string * string) -> string list option 13 14 (* Reconstruction *) 15 val mk_metis_call : string list -> string 16 val hh_reconstruct : string list -> goal -> (string * tactic) 17 18end 19