src/HOL/BNF/BNF_LFP.thy
changeset 53305 29c267cb9314
parent 52913 2d2d9d1de1a9
child 53309 42a99f732a40
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 11:37:22 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:05:22 2013 +0200
@@ -1,6 +1,8 @@
 (*  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.
 *)
@@ -10,7 +12,8 @@
 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> {}"
@@ -232,5 +235,6 @@
 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