# 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