src/HOL/Sledgehammer.thy
changeset 38025 b660597a6796
parent 38023 962b0a7f544b
child 38027 505657ddb047
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 18:38:10 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 18:45:55 2010 +0200
     1.3 @@ -10,17 +10,17 @@
     1.4  theory Sledgehammer
     1.5  imports Plain Hilbert_Choice
     1.6  uses
     1.7 -  "~~/src/Tools/Metis/metis.ML"
     1.8 +  ("Tools/ATP_Manager/async_manager.ML")
     1.9 +  ("Tools/ATP_Manager/atp_problem.ML")
    1.10 +  ("Tools/ATP_Manager/atp_systems.ML")
    1.11 +  ("~~/src/Tools/Metis/metis.ML")
    1.12    ("Tools/Sledgehammer/clausifier.ML")
    1.13    ("Tools/Sledgehammer/meson_tactic.ML")
    1.14    ("Tools/Sledgehammer/metis_clauses.ML")
    1.15    ("Tools/Sledgehammer/metis_tactics.ML")
    1.16    ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.17    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    1.18 -  ("Tools/ATP_Manager/atp_problem.ML")
    1.19    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.20 -  ("Tools/ATP_Manager/async_manager.ML")
    1.21 -  ("Tools/ATP_Manager/atp_systems.ML")
    1.22    ("Tools/Sledgehammer/sledgehammer.ML")
    1.23    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.24    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.25 @@ -85,6 +85,12 @@
    1.26  apply (simp add: COMBC_def) 
    1.27  done
    1.28  
    1.29 +use "Tools/ATP_Manager/async_manager.ML"
    1.30 +use "Tools/ATP_Manager/atp_problem.ML"
    1.31 +use "Tools/ATP_Manager/atp_systems.ML"
    1.32 +setup ATP_Systems.setup
    1.33 +
    1.34 +use "~~/src/Tools/Metis/metis.ML"
    1.35  use "Tools/Sledgehammer/clausifier.ML"
    1.36  use "Tools/Sledgehammer/meson_tactic.ML"
    1.37  setup Meson_Tactic.setup
    1.38 @@ -94,11 +100,7 @@
    1.39  
    1.40  use "Tools/Sledgehammer/sledgehammer_util.ML"
    1.41  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.42 -use "Tools/ATP_Manager/atp_problem.ML"
    1.43  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.44 -use "Tools/ATP_Manager/async_manager.ML"
    1.45 -use "Tools/ATP_Manager/atp_systems.ML"
    1.46 -setup ATP_Systems.setup
    1.47  use "Tools/Sledgehammer/sledgehammer.ML"
    1.48  setup Sledgehammer.setup
    1.49  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"