--- a/src/HOL/TPTP/atp_problem_import.ML Mon Apr 30 14:50:17 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Apr 30 21:59:10 2012 +0200
@@ -7,8 +7,18 @@
signature ATP_PROBLEM_IMPORT =
sig
+ val read_tptp_file :
+ theory -> (term -> term) -> string
+ -> term list * (term list * term list) * Proof.context
val nitpick_tptp_file : theory -> int -> string -> unit
val refute_tptp_file : theory -> int -> string -> unit
+ val can_tac : Proof.context -> tactic -> term -> bool
+ val SOLVE_TIMEOUT : int -> string -> tactic -> tactic
+ val atp_tac :
+ Proof.context -> (string * string) list -> int -> string -> int -> tactic
+ val smt_solver_tac : string -> Proof.context -> int -> tactic
+ val freeze_problem_consts : theory -> term -> term
+ val make_conj : term list * term list -> term list -> term
val sledgehammer_tptp_file : theory -> int -> string -> unit
val isabelle_demo_tptp_file : theory -> int -> string -> unit
val isabelle_comp_tptp_file : theory -> int -> string -> unit