--- a/prio/Paper/Paper.thy	Sun Feb 12 04:45:20 2012 +0000
+++ b/prio/Paper/Paper.thy	Sun Feb 12 05:06:59 2012 +0000
@@ -25,6 +25,7 @@
   dependents ("dependants") and
   cp ("cprec") and
   holdents ("resources") and
+  original_priority ("priority") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -203,6 +204,7 @@
   \end{isabelle}
 
   \noindent
+  In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
   Another function calculates the priority for a thread @{text "th"}, which is 
   defined as
 
@@ -350,7 +352,7 @@
   state @{text s}. It is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cpreced_def2}\numbered{permprops}
+  @{thm cpreced_def2}\hfill\numbered{cpreced}
   \end{isabelle}
 
   \noindent
@@ -374,14 +376,14 @@
   \end{isabelle}
 
   \noindent
-  The first function is a waiting queue function (that is takes a @{text "cs"} and returns the
+  The first function is a waiting queue function (that is it takes a resource @{text "cs"} and returns the
   corresponding list of threads that wait for it), the second is a function that takes
-  a thread and returns its current precedence (see ???). We assume the usual getter and 
+  a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and 
   setter methods for such records.
 
   In the initial state, the scheduler starts with all resources unlocked and the
   current precedence of every thread is initialised with @{term "Prc 0 0"}; that means 
-  @{abbrev initial_cprec}. Therefore
+  \mbox{@{abbrev initial_cprec}}. Therefore
   we have
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -470,7 +472,7 @@
   \end{isabelle}
 
   Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
-  @{term waiting}, @{term holding} @{term depend} and @{term cp} such that they only depend 
+  @{term waiting}, @{term holding}, @{term depend} and @{term cp} such that they only depend 
   on states.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -483,7 +485,8 @@
   \end{isabelle}
 
   \noindent
-  With them we can introduce the notion of threads being @{term readys} (i.e.~threads
+  With these abbreviations we can introduce for states 
+  the notion of threads being @{term readys} (i.e.~threads
   that do not wait for any resource) and the running thread.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -494,11 +497,13 @@
   \end{isabelle}
 
   \noindent
+  In this definition @{term "f ` S"} stands for the set @{text S} under the image of the 
+  function @{text f}. 
   Note that in the initial case, that is where the list of events is empty, the set 
   @{term threads} is empty and therefore there is no thread ready nor a running.
   If there is one or more threads ready, then there can only be \emph{one} thread
   running, namely the one whose current precedence is equal to the maximum of all ready 
-  threads. We can also define the set of resources that are locked by a thread in a
+  threads. We can also define the set of resources that are locked by a thread in any
   given state.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -508,9 +513,9 @@
   \noindent
   These resources are given by the holding edges in the RAG.
 
-  Finally we can define what a \emph{valid state} is. For example we cannot exptect to
+  Finally we can define what a \emph{valid state} is in our PIP. For example we cannot exptect to
   be able to exit a thread, if it was not created yet. These validity constraints
-  are characterised by the inductive predicate @{term "step"} by the following five 
+  are characterised by the inductive predicate @{term "step"}. We give five 
   inference rules relating a state and an event that can happen next.
 
   \begin{center}