src/HOL/ATP.thy

--- a/src/HOL/ATP.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/ATP.thy	Tue Oct 26 12:17:19 2010 +0200
@@ -6,11 +6,10 @@
 header {* Automatic Theorem Provers (ATPs) *}
 
 theory ATP
-imports HOL
-uses
-  "Tools/ATP/atp_problem.ML"
-  "Tools/ATP/atp_proof.ML"
-  "Tools/ATP/atp_systems.ML"
+imports Plain
+uses "Tools/ATP/atp_problem.ML"
+     "Tools/ATP/atp_proof.ML"
+     "Tools/ATP/atp_systems.ML"
 begin
 
 setup ATP_Systems.setup