src/HOL/BNF_LFP.thy
changeset 55530 3dfb724db099
parent 55084 8ee9aabb2bca
child 55531 601ca8efa000
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -13,8 +13,7 @@
     1.4  imports BNF_FP_Base
     1.5  keywords
     1.6    "datatype_new" :: thy_decl and
     1.7 -  "datatype_new_compat" :: thy_decl and
     1.8 -  "primrec_new" :: thy_decl
     1.9 +  "datatype_new_compat" :: thy_decl
    1.10  begin
    1.11  
    1.12  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"