src/HOL/ATP_Linkup.thy
changeset 32327 0971cc0b6a57
parent 31828 b686d4df54c2
child 32864 a226f29d4bdc
     1.1 --- a/src/HOL/ATP_Linkup.thy	Tue Aug 04 16:13:16 2009 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Tue Aug 04 19:20:24 2009 +0200
     1.3 @@ -15,9 +15,9 @@
     1.4    ("Tools/res_hol_clause.ML")
     1.5    ("Tools/res_reconstruct.ML")
     1.6    ("Tools/res_atp.ML")
     1.7 -  ("Tools/atp_manager.ML")
     1.8 -  ("Tools/atp_wrapper.ML")
     1.9 -  ("Tools/atp_minimal.ML")
    1.10 +  ("Tools/ATP_Manager/atp_manager.ML")
    1.11 +  ("Tools/ATP_Manager/atp_wrapper.ML")
    1.12 +  ("Tools/ATP_Manager/atp_minimal.ML")
    1.13    "~~/src/Tools/Metis/metis.ML"
    1.14    ("Tools/metis_tools.ML")
    1.15  begin
    1.16 @@ -96,10 +96,9 @@
    1.17  use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
    1.18  use "Tools/res_atp.ML"
    1.19  
    1.20 -use "Tools/atp_manager.ML"
    1.21 -use "Tools/atp_wrapper.ML"
    1.22 -
    1.23 -use "Tools/atp_minimal.ML"
    1.24 +use "Tools/ATP_Manager/atp_manager.ML"
    1.25 +use "Tools/ATP_Manager/atp_wrapper.ML"
    1.26 +use "Tools/ATP_Manager/atp_minimal.ML"
    1.27  
    1.28  text {* basic provers *}
    1.29  setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}