--- a/src/HOL/IMP/Def_Init_Sound_Small.thy Wed May 22 22:56:17 2013 +0200
+++ b/src/HOL/IMP/Def_Init_Sound_Small.thy Thu May 23 11:39:40 2013 +1000
@@ -49,7 +49,7 @@
theorem D_sound:
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
- \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs'' \<or> c' = SKIP"
+ \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
apply(induction arbitrary: A' rule:star_induct)
apply (metis progress)
by (metis D_preservation)