--- a/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 22:36:27 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 22:36:27 2012 +0200
@@ -3,6 +3,7 @@
*)
header {* ATP Problem Importer *}
+
theory ATP_Problem_Import
imports Complex_Main TPTP_Interpret
uses "sledgehammer_tactics.ML"