# HG changeset patch
# User blanchet
# Date 1286225513 -7200
# Node ID f95834c8bb4d4debff8cdf7ac198112261571604
# Parent  78faa9b312029a38cc6105ef839ea0a84d3ab3d9
tuning

diff -r 78faa9b31202 -r f95834c8bb4d src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Mon Oct 04 22:45:09 2010 +0200
+++ b/src/HOL/Meson.thy	Mon Oct 04 22:51:53 2010 +0200
@@ -5,7 +5,7 @@
     Copyright   2001  University of Cambridge
 *)
 
-header {* MESON Proof Procedure (Model Elimination) *}
+header {* MESON Proof Method *}
 
 theory Meson
 imports Datatype
diff -r 78faa9b31202 -r f95834c8bb4d src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Mon Oct 04 22:45:09 2010 +0200
+++ b/src/HOL/Metis.thy	Mon Oct 04 22:51:53 2010 +0200
@@ -29,7 +29,6 @@
 use "Tools/Metis/metis_translate.ML"
 use "Tools/Metis/metis_reconstruct.ML"
 use "Tools/Metis/metis_tactics.ML"
-
 setup Metis_Tactics.setup
 
 end
diff -r 78faa9b31202 -r f95834c8bb4d src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Oct 04 22:45:09 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Oct 04 22:51:53 2010 +0200
@@ -9,32 +9,22 @@
 
 theory Sledgehammer
 imports Plain
-uses
-  ("Tools/ATP/atp_problem.ML")
-  ("Tools/ATP/atp_proof.ML")
-  ("Tools/ATP/atp_systems.ML")
-  ("Tools/Sledgehammer/sledgehammer_util.ML")
-  ("Tools/Sledgehammer/sledgehammer_filter.ML")
-  ("Tools/Sledgehammer/sledgehammer_translate.ML")
-  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
-  ("Tools/Sledgehammer/sledgehammer.ML")
-  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
-  ("Tools/Sledgehammer/sledgehammer_isar.ML")
+uses "Tools/ATP/atp_problem.ML"
+     "Tools/ATP/atp_proof.ML"
+     "Tools/ATP/atp_systems.ML"
+     "Tools/Sledgehammer/sledgehammer_util.ML"
+     "Tools/Sledgehammer/sledgehammer_filter.ML"
+     "Tools/Sledgehammer/sledgehammer_translate.ML"
+     "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
+     "Tools/Sledgehammer/sledgehammer.ML"
+     "Tools/Sledgehammer/sledgehammer_minimize.ML"
+     "Tools/Sledgehammer/sledgehammer_isar.ML"
 begin
 
-use "Tools/ATP/atp_problem.ML"
-use "Tools/ATP/atp_proof.ML"
-use "Tools/ATP/atp_systems.ML"
-setup ATP_Systems.setup
-
-use "Tools/Sledgehammer/sledgehammer_util.ML"
-use "Tools/Sledgehammer/sledgehammer_filter.ML"
-use "Tools/Sledgehammer/sledgehammer_translate.ML"
-use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
-use "Tools/Sledgehammer/sledgehammer.ML"
-setup Sledgehammer.setup
-use "Tools/Sledgehammer/sledgehammer_minimize.ML"
-use "Tools/Sledgehammer/sledgehammer_isar.ML"
-setup Sledgehammer_Isar.setup
+setup {*
+  ATP_Systems.setup
+  #> Sledgehammer.setup
+  #> Sledgehammer_Isar.setup
+*}
 
 end