--- a/src/HOL/IMP/Compiler.thy Wed Sep 28 10:35:56 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy Thu Sep 29 21:42:03 2011 +0200
@@ -252,7 +252,7 @@
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
-subsection "Preservation of sematics"
+subsection "Preservation of semantics"
lemma ccomp_bigstep:
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
--- a/src/HOL/IMP/HoareT.thy Wed Sep 28 10:35:56 2011 +0200
+++ b/src/HOL/IMP/HoareT.thy Thu Sep 29 21:42:03 2011 +0200
@@ -10,7 +10,7 @@
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
-text{* Proveability of Hoare triples in the proof system for total
+text{* Provability of Hoare triples in the proof system for total
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
@{text"\<turnstile>"} only in the one place where nontermination can arise: the
--- a/src/HOL/IMP/Small_Step.thy Wed Sep 28 10:35:56 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy Thu Sep 29 21:42:03 2011 +0200
@@ -46,7 +46,7 @@
declare small_step.intros[simp,intro]
-text{* So called transitivity rules. See below. *}
+text{* So-called transitivity rules. See below. *}
declare step[trans] step1[trans]