src/HOL/BNF/BNF_LFP.thy

 (*  Title:      HOL/BNF/BNF_LFP.thy
     Author:     Dmitriy Traytel, TU Muenchen
-    Copyright   2012
+    Author:     Lorenz Panny, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013
 
 Least fixed point operation on bounded natural functors.
 *)
 
 header {* Least Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_LFP
 imports BNF_FP_Basic
 keywords
-  "datatype_new" :: thy_decl
+  "datatype_new" :: thy_decl and
+  "datatype_compat" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
 by blast
 

   unfolding vimage2p_def by auto
 
 ML_file "Tools/bnf_lfp_util.ML"
 ML_file "Tools/bnf_lfp_tactics.ML"
 ML_file "Tools/bnf_lfp.ML"
+ML_file "Tools/bnf_lfp_compat.ML"
 
 end