src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 55936 f6591f8c629d
parent 55811 aa1acc25126b
child 56011 39d5043ce8a3
     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