slightly clearer formulation
authorkleing
Thu May 23 11:39:40 2013 +1000 (2013-05-23)
changeset 52120e6433b34364b
parent 52119 90ba620333d0
child 52121 5b889b1b465b
slightly clearer formulation
src/HOL/IMP/Def_Init_Sound_Small.thy
     1.1 --- a/src/HOL/IMP/Def_Init_Sound_Small.thy	Wed May 22 22:56:17 2013 +0200
     1.2 +++ b/src/HOL/IMP/Def_Init_Sound_Small.thy	Thu May 23 11:39:40 2013 +1000
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5  theorem D_sound:
     1.6    "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
     1.7 -   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs'' \<or>  c' = SKIP"
     1.8 +   \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
     1.9  apply(induction arbitrary: A' rule:star_induct)
    1.10  apply (metis progress)
    1.11  by (metis D_preservation)