equal
deleted
inserted
replaced
3 Copyright 2012 |
3 Copyright 2012 |
4 |
4 |
5 Well-order embeddings as needed by bounded natural functors. |
5 Well-order embeddings as needed by bounded natural functors. |
6 *) |
6 *) |
7 |
7 |
8 header {* Well-Order Embeddings as Needed by Bounded Natural Functors *} |
8 section {* Well-Order Embeddings as Needed by Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_Wellorder_Embedding |
10 theory BNF_Wellorder_Embedding |
11 imports Hilbert_Choice BNF_Wellorder_Relation |
11 imports Hilbert_Choice BNF_Wellorder_Relation |
12 begin |
12 begin |
13 |
13 |