src/HOL/TPTP/atp_problem_import.ML

--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 20:08:33 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 22:00:33 2012 +0200
@@ -7,10 +7,10 @@
 
 signature ATP_PROBLEM_IMPORT =
 sig
-  val isabelle_tptp_file : int -> string -> unit
   val nitpick_tptp_file : int -> string -> unit
   val refute_tptp_file : int -> string -> unit
   val sledgehammer_tptp_file : int -> string -> unit
+  val isabelle_tptp_file : int -> string -> unit
   val translate_tptp_file : string -> string -> string -> unit
 end;
 
@@ -49,11 +49,6 @@
      Theory.checkpoint thy)
   end
 
-(** Isabelle (combination of provers) **)
-
-fun isabelle_tptp_file timeout file_name = ()
-
-
 (** Nitpick (alias Nitrox) **)
 
 fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
@@ -121,8 +116,25 @@
 
 (** Sledgehammer **)
 
-fun sledgehammer_tptp_file timeout file_name = ()
+fun apply_tactic_to_tptp_file tactic timeout file_name =
+  let
+    val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
+    val ctxt = Proof_Context.init_global thy
+  in
+    Goal.prove ctxt [] (defs @ nondefs) (hd conjs) (fn _ => tactic ctxt
+  end
 
+val sledgehammer_tptp_file =
+  apply_tactic_to_tptp_file Sledgehammer_Tactics.sledgehammer_as_oracle_tac
+
+
+(** Isabelle (combination of provers) **)
+
+val isabelle_tac =
+  ...
+
+val isabelle_tptp_file =
+  ...
 
 (** Translator between TPTP(-like) file formats **)