# HG changeset patch
# User haftmann
# Date 1288006497 -7200
# Node ID e7a80c6752c905a55d74ab3f39d79fa302257a13
# Parent  c57fffa2727c3c19aca23cbeb06d558139036f64
moved sledgehammer to Plain; tuned dependencies

diff -r c57fffa2727c -r e7a80c6752c9 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Mon Oct 25 13:34:57 2010 +0200
+++ b/src/HOL/ATP.thy	Mon Oct 25 13:34:57 2010 +0200
@@ -6,10 +6,11 @@
 header {* Automatic Theorem Provers (ATPs) *}
 
 theory ATP
-imports Plain
-uses "Tools/ATP/atp_problem.ML"
-     "Tools/ATP/atp_proof.ML"
-     "Tools/ATP/atp_systems.ML"
+imports HOL
+uses
+  "Tools/ATP/atp_problem.ML"
+  "Tools/ATP/atp_proof.ML"
+  "Tools/ATP/atp_systems.ML"
 begin
 
 setup ATP_Systems.setup
diff -r c57fffa2727c -r e7a80c6752c9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Oct 25 13:34:57 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Oct 25 13:34:57 2010 +0200
@@ -144,6 +144,7 @@
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
+  ATP.thy \
   Complete_Lattice.thy \
   Complete_Partial_Order.thy \
   Datatype.thy \
@@ -169,6 +170,7 @@
   Rings.thy \
   SAT.thy \
   Set.thy \
+  Sledgehammer.thy \
   Sum_Type.thy \
   Tools/abel_cancel.ML \
   Tools/arith_data.ML \
@@ -237,7 +239,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
-  ATP.thy \
   Big_Operators.thy \
   Code_Evaluation.thy \
   Code_Numeral.thy \
@@ -268,7 +269,6 @@
   Refute.thy \
   Semiring_Normalization.thy \
   SetInterval.thy \
-  Sledgehammer.thy \
   SMT.thy \
   String.thy \
   Typerep.thy \
diff -r c57fffa2727c -r e7a80c6752c9 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Oct 25 13:34:57 2010 +0200
+++ b/src/HOL/Main.thy	Mon Oct 25 13:34:57 2010 +0200
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Record Predicate_Compile Nitpick SMT
+imports Plain Record Predicate_Compile Nitpick SMT Quotient
 begin
 
 text {*
diff -r c57fffa2727c -r e7a80c6752c9 src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Mon Oct 25 13:34:57 2010 +0200
+++ b/src/HOL/Plain.thy	Mon Oct 25 13:34:57 2010 +0200
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Extraction Metis
+imports Datatype FunDef Extraction Sledgehammer
 begin
 
 text {*
diff -r c57fffa2727c -r e7a80c6752c9 src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Mon Oct 25 13:34:57 2010 +0200
+++ b/src/HOL/Refute.thy	Mon Oct 25 13:34:57 2010 +0200
@@ -8,7 +8,7 @@
 header {* Refute *}
 
 theory Refute
-imports Hilbert_Choice List Sledgehammer
+imports Hilbert_Choice List
 uses "Tools/refute.ML"
 begin
 
diff -r c57fffa2727c -r e7a80c6752c9 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Oct 25 13:34:57 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Oct 25 13:34:57 2010 +0200
@@ -7,7 +7,7 @@
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports ATP
+imports ATP Metis
 uses "Tools/Sledgehammer/sledgehammer_util.ML"
      "Tools/Sledgehammer/sledgehammer_filter.ML"
      "Tools/Sledgehammer/sledgehammer_atp_translate.ML"