--- a/prio/Paper/Paper.thy	Sat Feb 11 12:29:52 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 11 19:39:50 2012 +0000
@@ -185,7 +185,7 @@
   a thread obtains a new priority given by the programmer or
   user (for example via the {\tt nice} utility under UNIX).  As in Paulson's work, we
   need to define functions that allow one to make some observations
-  about states.  One, called @{term threads}, calculates, given a state @{text s}, the set of
+  about states.  One, called @{term threads}, calculates the set of
   ``live'' threads that we have seen so far:
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -305,14 +305,22 @@
   An instance of a RAG is as follows:
 
   \begin{center}
+  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
   \begin{tikzpicture}[scale=1]
-  \draw[step=2mm] (0,0) grid (3,2);
+  %%\draw[step=2mm] (-3,2) grid (1,-1);
 
-  \draw[rounded corners=1mm, very thick] (0,0) rectangle (0.6,0.6);
-  \draw[rounded corners=1mm, very thick] (3,0) rectangle (3.6,0.6);
+  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
+  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
+  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
+  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
+  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
 
-  \draw (0.3,0.3) node {\small$th_0$};
-  \draw (3.3,0.3) node {\small$th_1$};
+  \draw [->,line width=0.6mm] (A) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding}  (B);
+  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
+  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
+  \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding}  (E);
+  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}waiting}  (E);
   \end{tikzpicture}
   \end{center}