--- a/Journal/Paper.thy	Thu Jun 29 15:31:24 2017 +0100
+++ b/Journal/Paper.thy	Mon Jul 03 13:31:20 2017 +0100
@@ -206,8 +206,7 @@
   reader.  As we shall see, a correct version of PIP does not need to
   maintain this (potentially expensive) data structure at
   all. Surprisingly also the widely read and frequently updated
-  textbook \cite{Silberschatz13} gives the wrong specification. For
-  example on Page 254 the authors write: ``{\it Upon releasing the
+  textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the
   lock, the [low-priority] thread will revert to its original
   priority.}'' The same error is also repeated later in this popular textbook.
 
@@ -315,7 +314,7 @@
   verification \cite{Paulson98}. In this approach a \emph{state} of a system is
   given by a list of events that happened so far (with new events prepended to the list). 
   \emph{Events} of PIP fall
-  into five categories defined as the datatype:
+  into five categories defined as the Isabelle datatype:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
@@ -420,9 +419,10 @@
   @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}.
   \end{isabelle}
 
+  \noindent
   where we use Isabelle's notation for list-comprehensions. This
-  notation is very similar to notation used in Haskell for list
-  comprehensions.  A \emph{precedence} of a thread @{text th} in a
+  notation is very similar to notation used in Haskell for list-comprehensions.  
+  A \emph{precedence} of a thread @{text th} in a
   state @{text s} is the pair of natural numbers defined as
   
   \begin{isabelle}\ \ \ \ \ %%%

Binary file journal.pdf has changed