src/HOL/BNF_Wellorder_Embedding.thy
changeset 55059 ef2e0fb783c6
parent 55056 b5c94200d081
child 55101 57c875e488bd
     1.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -2,10 +2,10 @@
     1.4      Author:     Andrei Popescu, TU Muenchen
     1.5      Copyright   2012
     1.6  
     1.7 -Well-order embeddings (BNF).
     1.8 +Well-order embeddings as needed by bounded natural functors.
     1.9  *)
    1.10  
    1.11 -header {* Well-Order Embeddings (BNF) *}
    1.12 +header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
    1.13  
    1.14  theory BNF_Wellorder_Embedding
    1.15  imports Zorn BNF_Wellorder_Relation