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