src/HOL/Codatatype/BNF_Def.thy
changeset 49509 163914705f8d
parent 49495 675b9df572df
equal deleted inserted replaced
49508:1e205327f059 49509:163914705f8d
     1 (*  Title:      HOL/Codatatype/BNF_Def.thy
     1 (*  Title:      HOL/BNF/BNF_Def.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     3     Copyright   2012
     4 
     4 
     5 Definition of bounded natural functors.
     5 Definition of bounded natural functors.
     6 *)
     6 *)