reorder ML files in theory
authorblanchet
Tue Jul 27 18:45:55 2010 +0200 (2010-07-27)
changeset 38025b660597a6796
parent 38024 e4a95eb5530e
child 38026 bdd19b641062
reorder ML files in theory
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_problem.ML
     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"
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:38:10 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:45:55 2010 +0200
     2.3 @@ -32,8 +32,6 @@
     2.4  structure ATP_Problem : ATP_PROBLEM =
     2.5  struct
     2.6  
     2.7 -open Sledgehammer_Util
     2.8 -
     2.9  (** ATP problem **)
    2.10  
    2.11  datatype 'a fo_term = ATerm of 'a * 'a fo_term list