# HG changeset patch
# User blanchet
# Date 1335815950 -7200
# Node ID 2a2bc13669bd47548423435042c387499d65ab5e
# Parent  064394a1afb7e0ebcc8769824f4f8705fffb9bde
export more symbols

diff -r 064394a1afb7 -r 2a2bc13669bd src/HOL/TPTP/atp_problem_import.ML
--- 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