# HG changeset patch
# User traytel
# Date 1394111709 -3600
# Node ID f6591f8c629d2189b4eeceae3dd422d7a855d063
# Parent  8f20d09d294ef51c6da55f60a5d3f6e0231a6eed
rationalized imports

diff -r 8f20d09d294e -r f6591f8c629d src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 06 14:15:09 2014 +0100
@@ -8,7 +8,7 @@
 header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
 
 theory BNF_Cardinal_Order_Relation
-imports BNF_Constructions_on_Wellorders
+imports Zorn BNF_Constructions_on_Wellorders
 begin
 
 text{* In this section, we define cardinal-order relations to be minim well-orders
diff -r 8f20d09d294e -r f6591f8c629d src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Thu Mar 06 14:15:09 2014 +0100
@@ -8,7 +8,7 @@
 header {* Composition of Bounded Natural Functors *}
 
 theory BNF_Comp
-imports Basic_BNFs
+imports BNF_Def
 begin
 
 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
diff -r 8f20d09d294e -r f6591f8c629d src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 14:15:09 2014 +0100
@@ -10,7 +10,7 @@
 header {* Shared Fixed Point Operations on Bounded Natural Functors *}
 
 theory BNF_FP_Base
-imports BNF_Comp
+imports BNF_Comp Basic_BNFs
 begin
 
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
diff -r 8f20d09d294e -r f6591f8c629d src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 06 14:15:09 2014 +0100
@@ -8,7 +8,7 @@
 header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
 
 theory BNF_Wellorder_Embedding
-imports Zorn BNF_Wellorder_Relation
+imports Hilbert_Choice BNF_Wellorder_Relation
 begin
 
 text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and