src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 58127 b7cab82f488e
parent 56191 159b0c88b4a4
child 58623 2db1df2c8467
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Sep 01 16:34:38 2014 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Sep 01 16:34:39 2014 +0200
@@ -8,7 +8,7 @@
 header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
 
 theory BNF_Cardinal_Order_Relation
-imports Zorn BNF_Constructions_on_Wellorders
+imports Zorn BNF_Wellorder_Constructions
 begin
 
 text{* In this section, we define cardinal-order relations to be minim well-orders