# HG changeset patch
# User blanchet
# Date 1283292195 -7200
# Node ID 7fba3ccc755aaecdea7ce4fb1e241741d61b40fe
# Parent  e34b099e477e6038759fa602eb00acf24020e956
finish moving file

diff -r e34b099e477e -r 7fba3ccc755a src/HOL/HOL.thy
--- 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
 
diff -r e34b099e477e -r 7fba3ccc755a src/HOL/Sledgehammer.thy
--- 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
diff -r e34b099e477e -r 7fba3ccc755a src/HOL/Tools/async_manager.ML
--- 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