| changeset 58889 | 5b7a9633cfa8 |
| parent 58623 | 2db1df2c8467 |
| child 60585 | 48fdff264eb2 |
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Nov 02 18:21:45 2014 +0100 @@ -5,7 +5,7 @@ Cardinal-order relations as needed by bounded natural functors. *) -header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} +section {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} theory BNF_Cardinal_Order_Relation imports Zorn BNF_Wellorder_Constructions