--- a/Journal/Paper.thy	Sat May 24 12:39:12 2014 +0100
+++ b/Journal/Paper.thy	Fri May 30 07:56:39 2014 +0100
@@ -850,7 +850,7 @@
   guarantee absence of indefinite Priority Inversion. For this we
   further have to assume that every thread gives up its resources
   after a finite amount of time. We found that this assumption is
-  awkward to formalise in our model. There are mainly two reasons:
+  awkward to formalise in our model. There are mainly two reasons for this:
   First, we do not specify what ``running'' the code of a thread
   means, for example by giving an operational semantics for machine
   instructions. Therefore we cannot characterise what are ``good''