src/HOL/Codatatype/BNF_Comp.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/BNF_Comp.thy	Tue Aug 28 17:16:00 2012 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Codatatype/BNF_Comp.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Copyright   2012
+
+Composition of bounded natural functors.
+*)
+
+header {* Composition of Bounded Natural Functors *}
+
+theory BNF_Comp
+imports Basic_BNFs
+keywords
+  "bnf_of_typ" :: thy_decl
+uses
+  "Tools/bnf_comp_tactics.ML"
+  "Tools/bnf_comp.ML"
+  "Tools/bnf_fp_util.ML"
+begin
+
+end