| changeset 58889 | 5b7a9633cfa8 |
| parent 55936 | f6591f8c629d |
| child 60585 | 48fdff264eb2 |
--- a/src/HOL/BNF_Wellorder_Embedding.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/BNF_Wellorder_Embedding.thy Sun Nov 02 18:21:45 2014 +0100 @@ -5,7 +5,7 @@ Well-order embeddings as needed by bounded natural functors. *) -header {* Well-Order Embeddings as Needed by Bounded Natural Functors *} +section {* Well-Order Embeddings as Needed by Bounded Natural Functors *} theory BNF_Wellorder_Embedding imports Hilbert_Choice BNF_Wellorder_Relation