src/HOL/IMP/Compiler.thy

    \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
    \<Longrightarrow> i' = size P' + j
    \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
 by (drule exec_appendL[where P'=P']) simp
 
-text{* Split the execution of a compound program up into the excution of its
+text{* Split the execution of a compound program up into the execution of its
 parts: *}
 
 lemma exec_append_trans[intro]:
   fixes i' i'' j'' :: int
   shows