# HG changeset patch
# User kleing
# Date 1369273180 -36000
# Node ID e6433b34364bfca4d28e5843584c980b5d93910f
# Parent  90ba620333d00a0420ee484bdd917a9d460b2cad
slightly clearer formulation

diff -r 90ba620333d0 -r e6433b34364b src/HOL/IMP/Def_Init_Sound_Small.thy
--- 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)