changeset 46251 | 8fbcbcf4380e |
parent 46246 | e69684c1c142 |
child 46346 | 10c18630612a |
--- a/src/HOL/IMP/Abs_Int1.thy Wed Jan 18 22:06:31 2012 +0100 +++ b/src/HOL/IMP/Abs_Int1.thy Thu Jan 19 09:51:42 2012 +0100 @@ -258,7 +258,7 @@ lemma domo_Top[simp]: "domo \<top> = {}" by(simp add: domo_def Top_st_def Top_option_def) -lemma bot_acom_Dom[simp]: "\<bottom>\<^sub>c c \<in> Com X" +lemma bot_acom_Com[simp]: "\<bottom>\<^sub>c c \<in> Com X" by(simp add: bot_acom_def Com_def domo_def set_annos_anno) lemma post_in_annos: "post c : set(annos c)"