--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/BNF_LFP.thy Tue Aug 28 17:16:00 2012 +0200
@@ -0,0 +1,20 @@
+(* Title: HOL/Codatatype/BNF_LFP.thy
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2012
+
+Least fixed point operation on bounded natural functors.
+*)
+
+header {* Least Fixed Point Operation on Bounded Natural Functors *}
+
+theory BNF_LFP
+imports BNF_Comp
+keywords
+ "bnf_data" :: thy_decl
+uses
+ "Tools/bnf_lfp_util.ML"
+ "Tools/bnf_lfp_tactics.ML"
+ "Tools/bnf_lfp.ML"
+begin
+
+end