# HG changeset patch
# User blanchet
# Date 1277471938 -7200
# Node ID 931f5948a32dfd17b34fb6496c576707ebadc177
# Parent  38968bbcec5ac05b624c1288699e3f3653f99417
move "MESON" up;
the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti

diff -r 38968bbcec5a -r 931f5948a32d src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Jun 25 15:16:22 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 15:18:58 2010 +0200
@@ -14,6 +14,7 @@
   "Tools/Sledgehammer/sledgehammer_util.ML"
   ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
+  ("Tools/Sledgehammer/meson_tactic.ML")
   ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
@@ -22,7 +23,6 @@
   ("Tools/ATP_Manager/atp_systems.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
-  ("Tools/Sledgehammer/meson_tactic.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
 begin
 
@@ -86,11 +86,11 @@
 done
 
 
-subsection {* Setup of external ATPs *}
-
 use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
 setup Sledgehammer_Fact_Preprocessor.setup
+use "Tools/Sledgehammer/meson_tactic.ML"
+setup Meson_Tactic.setup
 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
@@ -100,16 +100,6 @@
 setup ATP_Systems.setup
 use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
 use "Tools/Sledgehammer/sledgehammer_isar.ML"
-
-
-subsection {* The MESON prover *}
-
-use "Tools/Sledgehammer/meson_tactic.ML"
-setup Meson_Tactic.setup
-
-
-subsection {* The Metis prover *}
-
 use "Tools/Sledgehammer/metis_tactics.ML"
 setup Metis_Tactics.setup