move "MESON" up;
authorblanchet
Fri Jun 25 15:18:58 2010 +0200 (2010-06-25)
changeset 37569931f5948a32d
parent 37568 38968bbcec5a
child 37570 de5feddaa95c
move "MESON" up;
the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 15:16:22 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 15:18:58 2010 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    "Tools/Sledgehammer/sledgehammer_util.ML"
     1.5    ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
     1.6    ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
     1.7 +  ("Tools/Sledgehammer/meson_tactic.ML")
     1.8    ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
     1.9    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.10    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    1.11 @@ -22,7 +23,6 @@
    1.12    ("Tools/ATP_Manager/atp_systems.ML")
    1.13    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.14    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.15 -  ("Tools/Sledgehammer/meson_tactic.ML")
    1.16    ("Tools/Sledgehammer/metis_tactics.ML")
    1.17  begin
    1.18  
    1.19 @@ -86,11 +86,11 @@
    1.20  done
    1.21  
    1.22  
    1.23 -subsection {* Setup of external ATPs *}
    1.24 -
    1.25  use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.26  use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
    1.27  setup Sledgehammer_Fact_Preprocessor.setup
    1.28 +use "Tools/Sledgehammer/meson_tactic.ML"
    1.29 +setup Meson_Tactic.setup
    1.30  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
    1.31  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.32  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.33 @@ -100,16 +100,6 @@
    1.34  setup ATP_Systems.setup
    1.35  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.36  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.37 -
    1.38 -
    1.39 -subsection {* The MESON prover *}
    1.40 -
    1.41 -use "Tools/Sledgehammer/meson_tactic.ML"
    1.42 -setup Meson_Tactic.setup
    1.43 -
    1.44 -
    1.45 -subsection {* The Metis prover *}
    1.46 -
    1.47  use "Tools/Sledgehammer/metis_tactics.ML"
    1.48  setup Metis_Tactics.setup
    1.49