src/HOL/BNF_Comp.thy
changeset 55059 ef2e0fb783c6
parent 55058 4e700eb471d4
child 55062 6d3fad6f01c9
equal deleted inserted replaced
55058:4e700eb471d4 55059:ef2e0fb783c6
     1 (*  Title:      HOL/BNF/BNF_Comp.thy
     1 (*  Title:      HOL/BNF_Comp.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     3     Copyright   2012
     4 
     4 
     5 Composition of bounded natural functors.
     5 Composition of bounded natural functors.
     6 *)
     6 *)