--- a/src/HOL/IMP/Abs_Int1.thy Wed Apr 17 21:11:01 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Apr 17 21:23:35 2013 +0200
@@ -4,7 +4,6 @@
imports Abs_State
begin
-(* FIXME mv *)
instantiation acom :: (type) vars
begin
@@ -26,10 +25,6 @@
strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
-(* FIXME mv *)
-lemma post_in_annos: "post C \<in> set(annos C)"
-by(induction C) auto
-
subsection "Computable Abstract Interpretation"