--- a/src/HOL/Sledgehammer.thy Tue Oct 05 10:59:12 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Oct 05 11:10:37 2010 +0200
@@ -1,18 +1,14 @@
(* Title: HOL/Sledgehammer.thy
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Fabian Immler, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
*)
header {* Sledgehammer: Isabelle--ATP Linkup *}
theory Sledgehammer
-imports Plain
-uses "Tools/ATP/atp_problem.ML"
- "Tools/ATP/atp_proof.ML"
- "Tools/ATP/atp_systems.ML"
- "Tools/Sledgehammer/sledgehammer_util.ML"
+imports ATP
+uses "Tools/Sledgehammer/sledgehammer_util.ML"
"Tools/Sledgehammer/sledgehammer_filter.ML"
"Tools/Sledgehammer/sledgehammer_translate.ML"
"Tools/Sledgehammer/sledgehammer_reconstruct.ML"
@@ -22,8 +18,7 @@
begin
setup {*
- ATP_Systems.setup
- #> Sledgehammer.setup
+ Sledgehammer.setup
#> Sledgehammer_Isar.setup
*}