# HG changeset patch
# User Jean Pichon
# Date 1317325323 -7200
# Node ID fa3715b35370fd27bc9e6bd03fad4a34b0724af3
# Parent  2a0d7be998bb892596088c1df98a2bccd51302bd
fixed typos in IMP

diff -r 2a0d7be998bb -r fa3715b35370 src/HOL/IMP/Compiler.thy
--- 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)"
diff -r 2a0d7be998bb -r fa3715b35370 src/HOL/IMP/HoareT.thy
--- 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
diff -r 2a0d7be998bb -r fa3715b35370 src/HOL/IMP/Small_Step.thy
--- 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]