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)"

     2.1 --- a/src/HOL/IMP/HoareT.thy	Wed Sep 28 10:35:56 2011 +0200
     2.2 +++ b/src/HOL/IMP/HoareT.thy	Thu Sep 29 21:42:03 2011 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
     2.5  "\<Turnstile>\<^sub>t {P}c{Q}  \<equiv>  \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
     2.6  
     2.7 -text{* Proveability of Hoare triples in the proof system for total
     2.8 +text{* Provability of Hoare triples in the proof system for total
     2.9  correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
    2.10  inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
    2.11  @{text"\<turnstile>"} only in the one place where nontermination can arise: the

     3.1 --- a/src/HOL/IMP/Small_Step.thy	Wed Sep 28 10:35:56 2011 +0200
     3.2 +++ b/src/HOL/IMP/Small_Step.thy	Thu Sep 29 21:42:03 2011 +0200
     3.3 @@ -46,7 +46,7 @@
     3.4  
     3.5  declare small_step.intros[simp,intro]
     3.6  
     3.7 -text{* So called transitivity rules. See below. *}
     3.8 +text{* So-called transitivity rules. See below. *}
     3.9  
    3.10  declare step[trans] step1[trans]
    3.11