# HG changeset patch
# User nipkow
# Date 1347609702 -7200
# Node ID 023be49d7fb80f17ae46ea98024818f0541d0927
# Parent  207c333f61af475f8c1133abe67c1479ef6b6251
tuned

diff -r 207c333f61af -r 023be49d7fb8 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu Sep 13 17:20:44 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Sep 14 10:01:42 2012 +0200
@@ -28,8 +28,11 @@
    wt I X \<and> vars b \<subseteq> X \<and> wt P X \<and> wt C X \<and> wt Q X"
 by(auto simp add: wt_acom_def)
 
-lemma wt_post[simp]: "wt c  X \<Longrightarrow> wt (post c) X"
-by(induction c)(auto simp: wt_acom_def)
+lemma post_in_annos: "post C : set(annos C)"
+by(induction C) auto
+
+lemma wt_post[simp]: "wt C X \<Longrightarrow> wt (post C) X"
+by(simp add: wt_acom_def post_in_annos)
 
 lemma lpfp_inv:
 assumes "lpfp f x0 = Some x" and "\<And>x. P x \<Longrightarrow> P(f x)" and "P(bot x0)"
diff -r 207c333f61af -r 023be49d7fb8 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Thu Sep 13 17:20:44 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Fri Sep 14 10:01:42 2012 +0200
@@ -52,7 +52,7 @@
 definition wt_option where
 "wt opt X = (case opt of None \<Rightarrow> True | Some x \<Rightarrow> wt x X)"
 
-lemma wt_simps[simp]: "wt None X" "wt (Some x) X = wt x X"
+lemma wt_option_simps[simp]: "wt None X" "wt (Some x) X = wt x X"
 by(simp_all add: wt_option_def)
 
 instance ..