--- a/Paper/Paper.thy	Mon Feb 21 03:35:39 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 22 12:43:05 2011 +0000
@@ -823,7 +823,7 @@
   \end{lemma}
 
   \begin{proof}
-  By the preceding Lemma, we know that there exists a @{text "rhs"} such
+  By the preceding lemma, we know that there exists a @{text "rhs"} such
   that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
   and that the invariant holds for this equation. That means we 
   know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
@@ -897,7 +897,7 @@
   directly. The reader is invited to try. 
 
   Our proof will rely on some
-  \emph{taggingfunctions} defined over strings. Given the inductive hypothesis, it will 
+  \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 
   be easy to prove that the \emph{range} of these tagging-functions is finite
   (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
   With this we will be able to infer that the tagging-functions, seen as relations,
@@ -910,7 +910,7 @@
   \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
   and @{text y} are \emph{tag-related} provided
   \begin{center}
-  @{text "x =tag= y \<equiv> tag x = tag y"}
+  @{text "x =tag= y \<equiv> tag x = tag y"}.
   \end{center}
   \end{definition}