finish moving file
authorblanchet
Wed Sep 01 00:03:15 2010 +0200 (2010-09-01)
changeset 389907fba3ccc755a
parent 38989 e34b099e477e
child 38991 0e2798f30087
finish moving file
src/HOL/HOL.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/async_manager.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Aug 31 23:52:59 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 01 00:03:15 2010 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    "~~/src/Tools/induct.ML"
     1.5    ("~~/src/Tools/induct_tacs.ML")
     1.6    ("Tools/recfun_codegen.ML")
     1.7 +  "Tools/async_manager.ML"
     1.8    "Tools/try.ML"
     1.9  begin
    1.10  
     2.1 --- a/src/HOL/Sledgehammer.thy	Tue Aug 31 23:52:59 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Wed Sep 01 00:03:15 2010 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  theory Sledgehammer
     2.5  imports Plain Hilbert_Choice
     2.6  uses
     2.7 -  ("Tools/ATP/async_manager.ML")
     2.8    ("Tools/ATP/atp_problem.ML")
     2.9    ("Tools/ATP/atp_systems.ML")
    2.10    ("~~/src/Tools/Metis/metis.ML")
    2.11 @@ -89,7 +88,6 @@
    2.12  apply (simp add: COMBC_def) 
    2.13  done
    2.14  
    2.15 -use "Tools/ATP/async_manager.ML"
    2.16  use "Tools/ATP/atp_problem.ML"
    2.17  use "Tools/ATP/atp_systems.ML"
    2.18  setup ATP_Systems.setup
     3.1 --- a/src/HOL/Tools/async_manager.ML	Tue Aug 31 23:52:59 2010 +0200
     3.2 +++ b/src/HOL/Tools/async_manager.ML	Wed Sep 01 00:03:15 2010 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Tools/ATP/async_manager.ML
     3.5 +(*  Title:      HOL/Tools/async_manager.ML
     3.6      Author:     Fabian Immler, TU Muenchen
     3.7      Author:     Makarius
     3.8      Author:     Jasmin Blanchette, TU Muenchen