src/HOL/Sledgehammer.thy
changeset 38019 e207a64e1e0b
parent 37622 b3f572839570
child 38021 e024504943d1
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:32:55 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 17:43:11 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    ("Tools/Sledgehammer/metis_tactics.ML")
     1.5    ("Tools/Sledgehammer/sledgehammer_util.ML")
     1.6    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     1.7 -  ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
     1.8 +  ("Tools/ATP_Manager/atp_problem.ML")
     1.9    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.10    ("Tools/ATP_Manager/async_manager.ML")
    1.11    ("Tools/ATP_Manager/atp_manager.ML")
    1.12 @@ -94,7 +94,7 @@
    1.13  
    1.14  use "Tools/Sledgehammer/sledgehammer_util.ML"
    1.15  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.16 -use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    1.17 +use "Tools/ATP_Manager/atp_problem.ML"
    1.18  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.19  use "Tools/ATP_Manager/async_manager.ML"
    1.20  use "Tools/ATP_Manager/atp_manager.ML"