src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 55059 ef2e0fb783c6
parent 55056 b5c94200d081
child 55604 42e4e8c2e8dc
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -2,10 +2,10 @@
     1.4      Author:     Dmitriy Traytel, TU Muenchen
     1.5      Copyright   2012
     1.6  
     1.7 -Cardinal arithmetic (BNF).
     1.8 +Cardinal arithmetic as needed by bounded natural functors.
     1.9  *)
    1.10  
    1.11 -header {* Cardinal Arithmetic (BNF) *}
    1.12 +header {* Cardinal Arithmetic as Needed by Bounded Natural Functors *}
    1.13  
    1.14  theory BNF_Cardinal_Arithmetic
    1.15  imports BNF_Cardinal_Order_Relation