--- a/src/HOL/IMP/Abs_Int0.thy Tue Jan 17 18:25:36 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Jan 18 10:05:14 2012 +0100
@@ -341,10 +341,15 @@
apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Semi strip_eq_If strip_eq_While)
done
+lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
+
+lemma set_annos_anno: "set (annos (anno a c)) = {a}"
+by(induction c)(auto)
+
lemma le_iff_le_annos: "c1 \<sqsubseteq> c2 \<longleftrightarrow>
(annos c1, annos c2) : listrel{(x,y). x \<sqsubseteq> y} \<and> strip c1 = strip c2"
apply(induct c1 c2 rule: le_acom.induct)
-apply (auto simp: listrel.Nil listrel_Cons_iff listrel_app size_annos_same)
+apply (auto simp: listrel.Nil listrel_Cons_iff listrel_app size_annos_same2)
apply (metis listrel_app_same_size size_annos_same)+
done