--- 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
--- 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 \
--- 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 {*
--- 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 {*
--- 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
--- 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"