src/HOL/Sledgehammer.thy
changeset 38047 9033c03cc214
parent 38028 22dcaec5fa77
child 38282 319c59682c51
     1.1 --- a/src/HOL/Sledgehammer.thy	Wed Jul 28 19:01:34 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Jul 28 19:04:59 2010 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4  theory Sledgehammer
     1.5  imports Plain Hilbert_Choice
     1.6  uses
     1.7 -  ("Tools/ATP_Manager/async_manager.ML")
     1.8 -  ("Tools/ATP_Manager/atp_problem.ML")
     1.9 -  ("Tools/ATP_Manager/atp_systems.ML")
    1.10 +  ("Tools/ATP/async_manager.ML")
    1.11 +  ("Tools/ATP/atp_problem.ML")
    1.12 +  ("Tools/ATP/atp_systems.ML")
    1.13    ("~~/src/Tools/Metis/metis.ML")
    1.14    ("Tools/Sledgehammer/clausifier.ML")
    1.15    ("Tools/Sledgehammer/meson_tactic.ML")
    1.16 @@ -85,9 +85,9 @@
    1.17  apply (simp add: COMBC_def) 
    1.18  done
    1.19  
    1.20 -use "Tools/ATP_Manager/async_manager.ML"
    1.21 -use "Tools/ATP_Manager/atp_problem.ML"
    1.22 -use "Tools/ATP_Manager/atp_systems.ML"
    1.23 +use "Tools/ATP/async_manager.ML"
    1.24 +use "Tools/ATP/atp_problem.ML"
    1.25 +use "Tools/ATP/atp_systems.ML"
    1.26  setup ATP_Systems.setup
    1.27  
    1.28  use "~~/src/Tools/Metis/metis.ML"