Structure tttUnfold
signature tttUnfold =
sig
include Abbrev
(* tools *)
val find_script : string -> string
val unquoteString : string -> string -> string
val load_sigobj : unit -> unit
(* recording *)
val ttt_rewrite_thy : string -> unit
val ttt_record_thy : string -> unit
val ttt_rewrite : unit -> string list
val ttt_record : unit -> unit (* includes ttt_rewrite *)
(* evaluation (warning: only evaluate a theory after recording) *)
val ttt_parallel_eval : int -> string list -> unit
end
HOL 4, Kananaskis-13