changeset 53309 | 42a99f732a40 |
parent 53305 | 29c267cb9314 |
child 53310 | 8af01463b2d3 |
--- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:09:51 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:12:41 2013 +0200 @@ -13,7 +13,7 @@ imports BNF_FP_Basic keywords "datatype_new" :: thy_decl and - "datatype_compat" :: thy_decl + "datatype_new_compat" :: thy_decl begin lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"