src/HOL/BNF_Greatest_Fixpoint.thy

 section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close>
 
 theory BNF_Greatest_Fixpoint
 imports BNF_Fixpoint_Base String
 keywords
-  "codatatype" :: thy_decl and
-  "primcorecursive" :: thy_goal and
-  "primcorec" :: thy_decl
+  "codatatype" :: thy_defn and
+  "primcorecursive" :: thy_goal_defn and
+  "primcorec" :: thy_defn
 begin
 
 alias proj = Equiv_Relations.proj
 
 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"