# HG changeset patch
# User haftmann
# Date 1197282243 -3600
# Node ID 0792e02973ccf90d662cfa3032ea4b1d8fd6a460
# Parent  1feb9c008d3ae1b120fed0433f6da92b4341ac99
swtiched ATP_Linkup and PreList in theory hierarchy

diff -r 1feb9c008d3a -r 0792e02973cc src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Sun Dec 09 21:44:50 2007 +0100
+++ b/src/HOL/ATP_Linkup.thy	Mon Dec 10 11:24:03 2007 +0100
@@ -7,7 +7,7 @@
 header{* The Isabelle-ATP Linkup *}
 
 theory ATP_Linkup
-imports Divides Record Hilbert_Choice Presburger Relation_Power SAT Recdef Extraction 
+imports PreList Hilbert_Choice
    (*It must be a parent or a child of every other theory, to prevent theory-merge errors.*)
 uses
   "Tools/polyhash.ML"
diff -r 1feb9c008d3a -r 0792e02973cc src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Dec 09 21:44:50 2007 +0100
+++ b/src/HOL/List.thy	Mon Dec 10 11:24:03 2007 +0100
@@ -6,7 +6,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports PreList
+imports ATP_Linkup
 uses "Tools/string_syntax.ML"
 begin
 
diff -r 1feb9c008d3a -r 0792e02973cc src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Sun Dec 09 21:44:50 2007 +0100
+++ b/src/HOL/PreList.thy	Mon Dec 10 11:24:03 2007 +0100
@@ -7,7 +7,7 @@
 header {* A Basis for Building the Theory of Lists *}
 
 theory PreList
-imports ATP_Linkup
+imports Record Presburger SAT Recdef Extraction Relation_Power
 begin
 
 text {*