diff -r 45e1d324c493 -r f676a68935a0 Journal/Paper.thy --- a/Journal/Paper.thy Thu Jun 12 10:14:50 2014 +0100 +++ b/Journal/Paper.thy Tue Jul 15 17:25:53 2014 +0200 @@ -154,7 +154,7 @@ error is made in the textbook \cite[Section 2.3.1]{book} which specifies for a process that inherited a higher priority and exits a critical section ``{\it it resumes the priority it had at the point - of entry into the critical section}''. The same error can also be + of entry into the critical section}''. This error can also be found in the more recent textbook \cite[Page 119]{Laplante11} where the authors state: ``{\it when [the task] exits the critical section that caused the block, it reverts to the priority it had when it entered that