changeset 69913 | ca515cf61651 |
parent 69745 | aec42cee2521 |
child 71262 | a30278c8585f |
--- a/src/HOL/BNF_Composition.thy Thu Mar 14 16:35:58 2019 +0100 +++ b/src/HOL/BNF_Composition.thy Thu Mar 14 16:55:06 2019 +0100 @@ -11,8 +11,8 @@ theory BNF_Composition imports BNF_Def keywords - "copy_bnf" :: thy_decl and - "lift_bnf" :: thy_goal + "copy_bnf" :: thy_defn and + "lift_bnf" :: thy_goal_defn begin lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"