src/HOL/IMP/Abs_Int1.thy
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)"