# HG changeset patch
# User blanchet
# Date 1280336699 -7200
# Node ID 9033c03cc21478233ca8f887d71ca19a7161e5e6
# Parent  6659c15e742104a4a02a35c24c2294cfa3ca2a48
consequence of directory renaming

diff -r 6659c15e7421 -r 9033c03cc214 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 28 19:01:34 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 28 19:04:59 2010 +0200
@@ -268,9 +268,9 @@
   $(SRC)/Provers/Arith/combine_numerals.ML \
   $(SRC)/Provers/Arith/extract_common_term.ML \
   $(SRC)/Tools/Metis/metis.ML \
-  Tools/ATP_Manager/async_manager.ML \
-  Tools/ATP_Manager/atp_problem.ML \
-  Tools/ATP_Manager/atp_systems.ML \
+  Tools/ATP/async_manager.ML \
+  Tools/ATP/atp_problem.ML \
+  Tools/ATP/atp_systems.ML \
   Tools/choice_specification.ML \
   Tools/int_arith.ML \
   Tools/groebner.ML \
diff -r 6659c15e7421 -r 9033c03cc214 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Wed Jul 28 19:01:34 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Wed Jul 28 19:04:59 2010 +0200
@@ -10,9 +10,9 @@
 theory Sledgehammer
 imports Plain Hilbert_Choice
 uses
-  ("Tools/ATP_Manager/async_manager.ML")
-  ("Tools/ATP_Manager/atp_problem.ML")
-  ("Tools/ATP_Manager/atp_systems.ML")
+  ("Tools/ATP/async_manager.ML")
+  ("Tools/ATP/atp_problem.ML")
+  ("Tools/ATP/atp_systems.ML")
   ("~~/src/Tools/Metis/metis.ML")
   ("Tools/Sledgehammer/clausifier.ML")
   ("Tools/Sledgehammer/meson_tactic.ML")
@@ -85,9 +85,9 @@
 apply (simp add: COMBC_def) 
 done
 
-use "Tools/ATP_Manager/async_manager.ML"
-use "Tools/ATP_Manager/atp_problem.ML"
-use "Tools/ATP_Manager/atp_systems.ML"
+use "Tools/ATP/async_manager.ML"
+use "Tools/ATP/atp_problem.ML"
+use "Tools/ATP/atp_systems.ML"
 setup ATP_Systems.setup
 
 use "~~/src/Tools/Metis/metis.ML"
diff -r 6659c15e7421 -r 9033c03cc214 src/HOL/Tools/ATP/async_manager.ML
--- a/src/HOL/Tools/ATP/async_manager.ML	Wed Jul 28 19:01:34 2010 +0200
+++ b/src/HOL/Tools/ATP/async_manager.ML	Wed Jul 28 19:04:59 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/ATP_Manager/async_manager.ML
+(*  Title:      HOL/Tools/ATP/async_manager.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Makarius
     Author:     Jasmin Blanchette, TU Muenchen
diff -r 6659c15e7421 -r 9033c03cc214 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 28 19:01:34 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 28 19:04:59 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/ATP_Manager/atp_problem.ML
+(*  Title:      HOL/Tools/ATP/atp_problem.ML
     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     Author:     Jasmin Blanchette, TU Muenchen
 
diff -r 6659c15e7421 -r 9033c03cc214 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 28 19:01:34 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 28 19:04:59 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/ATP_Manager/atp_systems.ML
+(*  Title:      HOL/Tools/ATP/atp_systems.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen