summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/BNF_Cardinal_Order_Relation.thy

changeset 58889 | 5b7a9633cfa8 |

parent 58623 | 2db1df2c8467 |

child 60585 | 48fdff264eb2 |

1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Nov 02 18:21:14 2014 +0100 1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Nov 02 18:21:45 2014 +0100 1.3 @@ -5,7 +5,7 @@ 1.4 Cardinal-order relations as needed by bounded natural functors. 1.5 *) 1.6 1.7 -header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} 1.8 +section {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} 1.9 1.10 theory BNF_Cardinal_Order_Relation 1.11 imports Zorn BNF_Wellorder_Constructions