| 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