src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 58127 b7cab82f488e
parent 56191 159b0c88b4a4
child 58623 2db1df2c8467
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Sep 01 16:34:38 2014 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Sep 01 16:34:39 2014 +0200
     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 Zorn BNF_Constructions_on_Wellorders
     1.8 +imports Zorn BNF_Wellorder_Constructions
     1.9  begin
    1.10  
    1.11  text{* In this section, we define cardinal-order relations to be minim well-orders