src/HOL/BNF_Wellorder_Embedding.thy
changeset 55936 f6591f8c629d
parent 55811 aa1acc25126b
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 06 14:14:54 2014 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 06 14:15:09 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_Wellorder_Embedding
     1.7 -imports Zorn BNF_Wellorder_Relation
     1.8 +imports Hilbert_Choice BNF_Wellorder_Relation
     1.9  begin
    1.10  
    1.11  text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and