more moving around of ML files in "Sledgehammer.thy"
authorblanchet
Fri Jun 25 15:30:38 2010 +0200 (2010-06-25)
changeset 3757176e23303c7ff
parent 37570 de5feddaa95c
child 37572 a899f9506f39
more moving around of ML files in "Sledgehammer.thy"
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 15:22:12 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 15:30:38 2010 +0200
     1.3 @@ -11,16 +11,16 @@
     1.4  imports Plain Hilbert_Choice
     1.5  uses
     1.6    "~~/src/Tools/Metis/metis.ML"
     1.7 -  "Tools/Sledgehammer/sledgehammer_util.ML"
     1.8 -  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
     1.9    ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
    1.10    ("Tools/Sledgehammer/meson_tactic.ML")
    1.11 +  ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.12 +  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    1.13    ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
    1.14 -  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.15    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    1.16    ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
    1.17    ("Tools/ATP_Manager/atp_manager.ML")
    1.18    ("Tools/ATP_Manager/atp_systems.ML")
    1.19 +  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.20    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.21    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.22    ("Tools/Sledgehammer/metis_tactics.ML")
    1.23 @@ -85,19 +85,20 @@
    1.24  apply (simp add: COMBC_def) 
    1.25  done
    1.26  
    1.27 -
    1.28 -use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.29  use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
    1.30  setup Sledgehammer_Fact_Preprocessor.setup
    1.31  use "Tools/Sledgehammer/meson_tactic.ML"
    1.32  setup Meson_Tactic.setup
    1.33 +
    1.34 +use "Tools/Sledgehammer/sledgehammer_util.ML"
    1.35 +use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.36  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
    1.37 -use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.38  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.39  use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    1.40  use "Tools/ATP_Manager/atp_manager.ML"
    1.41  use "Tools/ATP_Manager/atp_systems.ML"
    1.42  setup ATP_Systems.setup
    1.43 +use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.44  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.45  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.46  use "Tools/Sledgehammer/metis_tactics.ML"
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:22:12 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:30:38 2010 +0200
     2.3 @@ -35,8 +35,6 @@
     2.4  structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
     2.5  struct
     2.6  
     2.7 -open Sledgehammer_FOL_Clause
     2.8 -
     2.9  type cnf_thm = thm * ((string * int) * thm)
    2.10  
    2.11  val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator