src/HOL/Sledgehammer.thy
changeset 36377 b3dce4c715d0
parent 36376 e83d52a52449
child 36394 1a48d18449d8
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Apr 23 18:06:41 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Apr 23 18:11:41 2010 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
     1.5    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     1.6    ("Tools/ATP_Manager/atp_manager.ML")
     1.7 -  ("Tools/ATP_Manager/atp_wrapper.ML")
     1.8 +  ("Tools/ATP_Manager/atp_systems.ML")
     1.9    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.10    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.11    ("Tools/Sledgehammer/meson_tactic.ML")
    1.12 @@ -101,7 +101,7 @@
    1.13  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.14  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.15  use "Tools/ATP_Manager/atp_manager.ML"
    1.16 -use "Tools/ATP_Manager/atp_wrapper.ML"
    1.17 +use "Tools/ATP_Manager/atp_systems.ML"
    1.18  setup ATP_Systems.setup
    1.19  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.20  use "Tools/Sledgehammer/sledgehammer_isar.ML"