| changeset 55936 | f6591f8c629d |
| parent 55935 | 8f20d09d294e |
| child 56016 | 8875cdcfc85b |
--- a/src/HOL/BNF_Comp.thy Thu Mar 06 14:14:54 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Thu Mar 06 14:15:09 2014 +0100 @@ -8,7 +8,7 @@ header {* Composition of Bounded Natural Functors *} theory BNF_Comp -imports Basic_BNFs +imports BNF_Def begin lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"