clarified import
authorhaftmann
Tue Jul 10 17:30:49 2007 +0200 (2007-07-10)
changeset 23708b5eb0b4dd17d
parent 23707 745799215e02
child 23709 fd31da8f752a
clarified import
src/HOL/Inductive.thy
src/HOL/Numeral.thy
src/HOL/PreList.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Inductive.thy	Tue Jul 10 17:30:47 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jul 10 17:30:49 2007 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Support for inductive sets and types *}
     1.5  
     1.6  theory Inductive 
     1.7 -imports FixedPoint Sum_Type Relation Record
     1.8 +imports FixedPoint Product_Type Sum_Type
     1.9  uses
    1.10    ("Tools/inductive_package.ML")
    1.11    ("Tools/old_inductive_package.ML")
     2.1 --- a/src/HOL/Numeral.thy	Tue Jul 10 17:30:47 2007 +0200
     2.2 +++ b/src/HOL/Numeral.thy	Tue Jul 10 17:30:49 2007 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Arithmetic on Binary Integers *}
     2.5  
     2.6  theory Numeral
     2.7 -imports IntDef
     2.8 +imports Datatype IntDef
     2.9  uses
    2.10    ("Tools/numeral.ML")
    2.11    ("Tools/numeral_syntax.ML")
     3.1 --- a/src/HOL/PreList.thy	Tue Jul 10 17:30:47 2007 +0200
     3.2 +++ b/src/HOL/PreList.thy	Tue Jul 10 17:30:49 2007 +0200
     3.3 @@ -7,8 +7,7 @@
     3.4  header {* A Basis for Building the Theory of Lists *}
     3.5  
     3.6  theory PreList
     3.7 -imports Wellfounded_Relations Presburger Relation_Power SAT
     3.8 -  FunDef Recdef Extraction
     3.9 +imports Presburger Relation_Power SAT Recdef Extraction Record
    3.10  begin
    3.11  
    3.12  text {*
    3.13 @@ -17,3 +16,4 @@
    3.14  *}
    3.15  
    3.16  end
    3.17 +
     4.1 --- a/src/HOL/Predicate.thy	Tue Jul 10 17:30:47 2007 +0200
     4.2 +++ b/src/HOL/Predicate.thy	Tue Jul 10 17:30:49 2007 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Predicates *}
     4.5  
     4.6  theory Predicate
     4.7 -imports Inductive
     4.8 +imports Inductive Relation
     4.9  begin
    4.10  
    4.11  subsection {* Converting between predicates and sets *}