--- a/src/HOL/IMP/Def_Init_Sound_Small.thy Wed Mar 20 11:32:16 2013 +0100
+++ b/src/HOL/IMP/Def_Init_Sound_Small.thy Wed Mar 20 14:56:30 2013 +0100
@@ -48,8 +48,8 @@
qed (auto intro: D.intros)
theorem D_sound:
- "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
- \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
+ "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
+ \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs'' \<or> c' = SKIP"
apply(induction arbitrary: A' rule:star_induct)
apply (metis progress)
by (metis D_preservation)