diff -r e3cf792db636 -r 0f124691c191 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Jun 14 15:06:16 2016 +0100
+++ b/Journal/Paper.thy	Fri Jun 17 09:46:25 2016 +0100
@@ -33,18 +33,21 @@
   vt ("valid'_state") and
   Prc ("'(_, _')") and
   holding_raw ("holds") and
-  holding ("Holds") and
+  holding ("holds") and
   waiting_raw ("waits") and
-  waiting ("Waits") and
+  waiting ("waits") and
   dependants_raw ("dependants") and
-  dependants ("Dependants") and
+  dependants ("dependants") and
+  RAG_raw ("RAG") and
+  RAG ("RAG") and
   Th ("T") and
   Cs ("C") and
   readys ("ready") and
   preced ("prec") and
   preceds ("precs") and
   cpreced ("cprec") and
-  cp ("cprec") and
+  wq_fun ("wq") and
+  cprec_fun ("cp") and
   holdents ("resources") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
   cntP ("c\<^bsub>P\<^esub>") and
@@ -455,7 +458,7 @@
   \noindent
   Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs} 
   (RAG), which represent the dependencies between threads and resources.
-  We represent RAGs as relations using pairs of the form
+  We choose to represent RAGs as relations using pairs of the form
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
@@ -524,8 +527,6 @@
   that the resource is locked. In this way we can always start at a thread waiting for a 
   resource and ``chase'' outgoing arrows leading to a single root of a tree. 
   
-
-
   The use of relations for representing RAGs allows us to conveniently define
   the notion of the \emph{dependants} of a thread using the transitive closure
   operation for relations, written ~@{term "trancl DUMMY"}. This gives
@@ -545,14 +546,14 @@
   there is a circle of dependencies in a RAG, then clearly we have a
   deadlock. Therefore when a thread requests a resource, we must
   ensure that the resulting RAG is not circular. In practice, the
-  programmer has to ensure this.
-
+  programmer has to ensure this. Our model will assume that critical 
+  reseources can only be requested provided no circularity can arise.
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cpreced_def2}\hfill\numbered{cpreced}
+  @{thm cpreced_def}\hfill\numbered{cpreced}
   \end{isabelle}
 
   \noindent
@@ -568,13 +569,17 @@
   lowered prematurely. We again introduce an abbreviation for current precedeces of
   a set of threads, written @{term "cprecs wq s ths"}.
   
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cpreceds_def}
+  \end{isabelle}
+
   The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
   by recursion on the state (a list of events); this function returns a \emph{schedule state}, which 
   we represent as a record consisting of two
   functions:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
+  @{text "\<lparr>wq, cp\<rparr>"}
   \end{isabelle}
 
   \noindent