# HG changeset patch
# User nipkow
# Date 1328035116 -3600
# Node ID d943f9da704a7da87fa09b11231e4dc358099f9e
# Parent  6b17c65d35c4c06d308aac87aa00eb2a60bae03a
tuned

diff -r 6b17c65d35c4 -r d943f9da704a src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Jan 31 18:46:31 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Jan 31 19:38:36 2012 +0100
@@ -620,7 +620,10 @@
   show ?thesis using assms(3) by(simp)
 qed
 
-(* step' = step_ivl! mv into locale*)
+
+context Abs_Int2
+begin
+
 lemma iter_widen_step'_Com:
   "iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X)
    \<Longrightarrow> c' : Com(X)"
@@ -632,8 +635,10 @@
 apply (auto simp: step'_Com)
 done
 
-theorem step_ivl_termination:
-  "EX c. AI_ivl' c0 = Some c"
+end
+
+theorem AI_ivl'_termination:
+  "EX c'. AI_ivl' c = Some c'"
 apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split)
 apply(rule iter_narrow_step_ivl_termination)
 apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step')