rationalized imports
authortraytel
Thu Mar 06 14:15:09 2014 +0100 (2014-03-06)
changeset 55936f6591f8c629d
parent 55935 8f20d09d294e
child 55937 18e52e8c6300
rationalized imports
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Comp.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_Wellorder_Embedding.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 06 14:14:54 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 06 14:15:09 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_Cardinal_Order_Relation
     1.7 -imports BNF_Constructions_on_Wellorders
     1.8 +imports Zorn BNF_Constructions_on_Wellorders
     1.9  begin
    1.10  
    1.11  text{* In this section, we define cardinal-order relations to be minim well-orders
     2.1 --- a/src/HOL/BNF_Comp.thy	Thu Mar 06 14:14:54 2014 +0100
     2.2 +++ b/src/HOL/BNF_Comp.thy	Thu Mar 06 14:15:09 2014 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Composition of Bounded Natural Functors *}
     2.5  
     2.6  theory BNF_Comp
     2.7 -imports Basic_BNFs
     2.8 +imports BNF_Def
     2.9  begin
    2.10  
    2.11  lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
     3.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 14:14:54 2014 +0100
     3.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 14:15:09 2014 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  header {* Shared Fixed Point Operations on Bounded Natural Functors *}
     3.5  
     3.6  theory BNF_FP_Base
     3.7 -imports BNF_Comp
     3.8 +imports BNF_Comp Basic_BNFs
     3.9  begin
    3.10  
    3.11  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     4.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 06 14:14:54 2014 +0100
     4.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 06 14:15:09 2014 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
     4.5  
     4.6  theory BNF_Wellorder_Embedding
     4.7 -imports Zorn BNF_Wellorder_Relation
     4.8 +imports Hilbert_Choice BNF_Wellorder_Relation
     4.9  begin
    4.10  
    4.11  text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and