src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 55059 ef2e0fb783c6
parent 55056 b5c94200d081
child 55087 252c7fec4119
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.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 -Cardinal-order relations (BNF).
     1.8 +Cardinal-order relations as needed by bounded natural functors.
     1.9  *)
    1.10  
    1.11 -header {* Cardinal-Order Relations (BNF) *}
    1.12 +header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
    1.13  
    1.14  theory BNF_Cardinal_Order_Relation
    1.15  imports BNF_Constructions_on_Wellorders