--- a/src/HOL/HOL.thy Tue Aug 31 23:52:59 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 01 00:03:15 2010 +0200
@@ -30,6 +30,7 @@
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
+ "Tools/async_manager.ML"
"Tools/try.ML"
begin
--- a/src/HOL/Sledgehammer.thy Tue Aug 31 23:52:59 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Sep 01 00:03:15 2010 +0200
@@ -10,7 +10,6 @@
theory Sledgehammer
imports Plain Hilbert_Choice
uses
- ("Tools/ATP/async_manager.ML")
("Tools/ATP/atp_problem.ML")
("Tools/ATP/atp_systems.ML")
("~~/src/Tools/Metis/metis.ML")
@@ -89,7 +88,6 @@
apply (simp add: COMBC_def)
done
-use "Tools/ATP/async_manager.ML"
use "Tools/ATP/atp_problem.ML"
use "Tools/ATP/atp_systems.ML"
setup ATP_Systems.setup
--- a/src/HOL/Tools/async_manager.ML Tue Aug 31 23:52:59 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML Wed Sep 01 00:03:15 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/ATP/async_manager.ML
+(* Title: HOL/Tools/async_manager.ML
Author: Fabian Immler, TU Muenchen
Author: Makarius
Author: Jasmin Blanchette, TU Muenchen