# HG changeset patch
# User blanchet
# Date 1434984963 -7200
# Node ID c5953e3a1e4f17e2f78063edf8a37b11fcaa3745
# Parent  4246da644cca942c32d40e7996c01b1332f0c9c4
fixed typo

diff -r 4246da644cca -r c5953e3a1e4f src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Mon Jun 22 11:15:23 2015 +0200
+++ b/src/HOL/IMP/Compiler.thy	Mon Jun 22 16:56:03 2015 +0200
@@ -146,7 +146,7 @@
    \<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]: