--- a/Journal/Paper.thy	Wed Jan 10 00:28:27 2018 +0000
+++ b/Journal/Paper.thy	Mon Jan 15 11:35:56 2018 +0000
@@ -362,10 +362,12 @@
   \end{tabular}}
   \end{isabelle}
 
-  \noindent
-  In this definition @{term "DUMMY # DUMMY"} stands for list-cons and @{term "[]"} for the empty list.
-  Another function calculates the priority for a thread @{text "th"}, which is 
-  defined as
+  \noindent In this definition @{term "DUMMY # DUMMY"} stands for
+  list-cons and @{term "[]"} for the empty list. We use @{term "DUMMY"}
+  to match any pattern, like in functional programming.
+  Another function
+  calculates the priority for a thread @{text "th"}, which is defined
+  as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -1174,7 +1176,7 @@
 
   \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state
   @{text "s"}, then, according to the definition of detached, @{text
-  "th’"} does not hold or wait for any resource. Hence the @{text
+  "th'"} does not hold or wait for any resource. Hence the @{text
   cp}-value of @{text "th'"} in @{text s} is not boosted, that is
   @{term "cp s th' = prec th' s"}, and is therefore lower than the
   precedence (as well as the @{text "cp"}-value) of @{term "th"}. This
@@ -1699,7 +1701,7 @@
   \end{quote} 
 
   \noindent By this assumption we enforce that any thread potentially
-  blocking @{term th} must become detached (that is lock no resource
+  blocking @{term th} must become detached (that is it owns no resource
   anymore) after a finite number of events in @{text "es @ s"}. Again
   we have to state this bound to hold in all valid states after @{text
   s}. The bound reflects how each thread @{text "th'"} is programmed: