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 *}