--- a/prio/Paper/Paper.thy	Wed Feb 22 13:25:49 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 27 18:53:53 2012 +0000
@@ -2,6 +2,15 @@
 theory Paper
 imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
 begin
+
+(*
+find_unused_assms CpsG 
+find_unused_assms ExtGG 
+find_unused_assms Moment 
+find_unused_assms Precedence_ord 
+find_unused_assms PrioG 
+find_unused_assms PrioGDef
+*)
 ML {*
   open Printer;
   show_question_marks_default := false;
@@ -313,7 +322,7 @@
   \end{isabelle}
 
   \noindent
-  Given three threads and three resources, an instance of a RAG can be pictured 
+  Given four threads and three resources, an instance of a RAG can be pictured 
   as follows:
 
   \begin{center}
@@ -501,7 +510,7 @@
   \end{isabelle}
 
   \noindent
-  With these abbreviations we can introduce 
+  With these abbreviations in place we can introduce 
   the notion of threads being @{term readys} in a state (i.e.~threads
   that do not wait for any resource) and the running thread.
 
@@ -626,15 +635,15 @@
 
   Even when fixed, their proof idea does not seem to go through for
   us, because of the way we have set up our formal model of PIP.  One
-  reason is that we allow that critical sections can intersect
+  reason is that we allow critical sections to intersect
   (something Sha et al.~explicitly exclude).  Therefore we have
   designed a different correctness criterion for PIP. The idea behind
   our criterion is as follows: for all states @{text s}, we know the
   corresponding thread @{text th} with the highest precedence; we show
   that in every future state (denoted by @{text "s' @ s"}) in which
   @{text th} is still alive, either @{text th} is running or it is
-  blocked by a thread that was alive in the state @{text s} and was in
-  the possession of a lock in @{text s}. Since in @{text s}, as in
+  blocked by a thread that was alive in the state @{text s} and was waiting 
+  or in the possession of a lock in @{text s}. Since in @{text s}, as in
   every state, the set of alive threads is finite, @{text th} can only
   be blocked a finite number of times. This is independent of how many
   threads of lower priority are created in @{text "s'"}. We will actually prove a
@@ -1068,7 +1077,7 @@
   and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
   the @{term "cp"} of every 
   thread encountered on the way. Since the @{term "depend"}
-  is loop free, this procedure will always stop. The following two lemmas show, however, 
+  is assumed to be loop free, this procedure will always stop. The following two lemmas show, however, 
   that this procedure can actually stop often earlier without having to consider all
   dependants.