Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
consequence of directory renaming
authorblanchet
Wed, 28 Jul 2010 19:04:59 +0200
changeset 38047 9033c03cc214
parent 38046 6659c15e7421
child 38048 9eda375ec19d
consequence of directory renaming
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Sledgehammer.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/ATP/async_manager.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- 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 \
--- 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"
--- 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
--- 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
 
--- 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
isabelle