1.1 --- a/src/HOL/IMP/Compiler.thy	Wed Sep 28 10:35:56 2011 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Sep 29 21:42:03 2011 +0200
     1.3 @@ -252,7 +252,7 @@
     1.4  value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
     1.5  
     1.6  
     1.7 -subsection "Preservation of sematics"
     1.8 +subsection "Preservation of semantics"
     1.9  
    1.10  lemma ccomp_bigstep:
    1.11    "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"