# HG changeset patch
# User nipkow
# Date 1366226615 -7200
# Node ID 30624dab6054c6b41ec97eaacc0bdcef64104073
# Parent  df3426139651121024bb64fe5a8ad134a08ea8b2
tuned

diff -r df3426139651 -r 30624dab6054 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Wed Apr 17 21:11:01 2013 +0200
+++ b/src/HOL/IMP/ACom.thy	Wed Apr 17 21:23:35 2013 +0200
@@ -134,4 +134,7 @@
 
 lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
 
+lemma post_in_annos: "post C \<in> set(annos C)"
+by(induction C) auto
+
 end
diff -r df3426139651 -r 30624dab6054 src/HOL/IMP/Abs_Int1.thy
--- 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"