--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ATP.thy	Tue Oct 05 11:10:37 2010 +0200
@@ -0,0 +1,17 @@
+(*  Title:      HOL/ATP.thy
+    Author:     Fabian Immler, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+*)
+
+header {* Sledgehammer: Isabelle--ATP Linkup *}
+
+theory ATP
+imports Plain
+uses "Tools/ATP/atp_problem.ML"
+     "Tools/ATP/atp_proof.ML"
+     "Tools/ATP/atp_systems.ML"
+begin
+
+setup ATP_Systems.setup
+
+end