swtiched ATP_Linkup and PreList in theory hierarchy
authorhaftmann
Mon Dec 10 11:24:03 2007 +0100 (2007-12-10)
changeset 255910792e02973cc
parent 25590 1feb9c008d3a
child 25592 e8ddaf6bf5df
swtiched ATP_Linkup and PreList in theory hierarchy
src/HOL/ATP_Linkup.thy
src/HOL/List.thy
src/HOL/PreList.thy
     1.1 --- a/src/HOL/ATP_Linkup.thy	Sun Dec 09 21:44:50 2007 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Mon Dec 10 11:24:03 2007 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header{* The Isabelle-ATP Linkup *}
     1.5  
     1.6  theory ATP_Linkup
     1.7 -imports Divides Record Hilbert_Choice Presburger Relation_Power SAT Recdef Extraction 
     1.8 +imports PreList Hilbert_Choice
     1.9     (*It must be a parent or a child of every other theory, to prevent theory-merge errors.*)
    1.10  uses
    1.11    "Tools/polyhash.ML"
     2.1 --- a/src/HOL/List.thy	Sun Dec 09 21:44:50 2007 +0100
     2.2 +++ b/src/HOL/List.thy	Mon Dec 10 11:24:03 2007 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* The datatype of finite lists *}
     2.5  
     2.6  theory List
     2.7 -imports PreList
     2.8 +imports ATP_Linkup
     2.9  uses "Tools/string_syntax.ML"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/PreList.thy	Sun Dec 09 21:44:50 2007 +0100
     3.2 +++ b/src/HOL/PreList.thy	Mon Dec 10 11:24:03 2007 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  header {* A Basis for Building the Theory of Lists *}
     3.5  
     3.6  theory PreList
     3.7 -imports ATP_Linkup
     3.8 +imports Record Presburger SAT Recdef Extraction Relation_Power
     3.9  begin
    3.10  
    3.11  text {*