Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authornipkow
Wed, 17 Apr 2013 21:23:35 +0200
changeset 51712 30624dab6054
parent 51711 df3426139651
child 51713 4fd969609b4d
child 51715 17b992f19b51
tuned
src/HOL/IMP/ACom.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/Abs_Int1.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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"
isabelle