1signature tacticToe = 2sig 3 4 include Abbrev 5 6 type tnn = mlTreeNeuralNetwork.tnn 7 8 val build_searchobj : mlThmData.thmdata * mlTacticData.tacdata -> 9 tnn option * tnn option * tnn option -> 10 goal -> tttSearch.searchobj 11 val main_tactictoe : 12 mlThmData.thmdata * mlTacticData.tacdata -> 13 tnn option * tnn option * tnn option -> 14 goal -> tttSearch.proofstatus * tttSearch.tree 15 16 val clean_ttt_tacdata_cache : unit -> unit 17 val set_timeout : real -> unit 18 val prioritize_stacl : string list ref 19 (* tactics on prioritize_stacl are added to tactictoe and 20 first tactics on the list are applied first *) 21 22 val ttt : tactic 23 val tactictoe : term -> thm 24 25 26end 27