src/HOL/ATP_Linkup.thy

 *)
 
 header{* The Isabelle-ATP Linkup *}
 
 theory ATP_Linkup
-imports Record Presburger SAT Recdef Extraction Relation_Power Hilbert_Choice
+imports Record Hilbert_Choice
 uses
   "Tools/polyhash.ML"
   "Tools/res_clause.ML"
   ("Tools/res_hol_clause.ML")
   ("Tools/res_axioms.ML")

 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBC_def) 
 done
 
+
+subsection {* Setup of Vampire, E prover and SPASS *}
+
 use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
 setup ResAxioms.setup
 
 use "Tools/res_hol_clause.ML"
 use "Tools/res_reconstruct.ML"
 use "Tools/watcher.ML"
 use "Tools/res_atp.ML"
-
-
-subsection {* Setup for Vampire, E prover and SPASS *}
 
 use "Tools/res_atp_provers.ML"
 
 oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
 oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}