src/HOL/Sledgehammer.thy
changeset 38023 962b0a7f544b
parent 38021 e024504943d1
child 38025 b660597a6796
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:58:30 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 18:33:10 2010 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4    ("Tools/ATP_Manager/atp_problem.ML")
     1.5    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
     1.6    ("Tools/ATP_Manager/async_manager.ML")
     1.7 -  ("Tools/ATP_Manager/atp_manager.ML")
     1.8    ("Tools/ATP_Manager/atp_systems.ML")
     1.9 +  ("Tools/Sledgehammer/sledgehammer.ML")
    1.10    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.11    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.12  begin
    1.13 @@ -97,9 +97,10 @@
    1.14  use "Tools/ATP_Manager/atp_problem.ML"
    1.15  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.16  use "Tools/ATP_Manager/async_manager.ML"
    1.17 -use "Tools/Sledgehammer/sledgehammer.ML"
    1.18  use "Tools/ATP_Manager/atp_systems.ML"
    1.19  setup ATP_Systems.setup
    1.20 +use "Tools/Sledgehammer/sledgehammer.ML"
    1.21 +setup Sledgehammer.setup
    1.22  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.23  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.24  setup Metis_Tactics.setup