--- a/Paper/Paper.thy	Thu Jun 20 23:28:26 2013 -0400
+++ b/Paper/Paper.thy	Tue Feb 25 20:01:47 2014 +0000
@@ -336,13 +336,13 @@
   \begin{tikzpicture}[scale=1]
   %%\draw[step=2mm] (-3,2) grid (1,-1);
 
-  \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 (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
-  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>0"}};
+  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>1"}};
+  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>1"}};
+  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>2"}};
+  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>2"}};
+  \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>3"}};
+  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>3"}};
 
   \draw [<-,line width=0.6mm] (A) to node [pos=0.54,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);
@@ -366,10 +366,10 @@
   This definition needs to account for all threads that wait for a thread to
   release a resource. This means we need to include threads that transitively
   wait for a resource being released (in the picture above this means the dependants
-  of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"}, 
-  but also @{text "th\<^isub>3"}, 
-  which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
-  in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies 
+  of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"}, 
+  but also @{text "th\<^sub>3"}, 
+  which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
+  in turn needs to wait for @{text "th\<^sub>0"} to finish). If 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 
@@ -763,9 +763,9 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
-  @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
-  @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
+  @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
+  @{thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
   \end{tabular}
   \end{isabelle}
 
@@ -864,7 +864,7 @@
   %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
   %  @   {thm [display] chain_building[rule_format]}
   %\item The ready thread chased to is unique (@{text "dchain_unique"}):
-  %  @   {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+  %  @   {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]}
   %\end{enumerate}
 
   %Some deeper results about the system:
@@ -1335,8 +1335,8 @@
   We are grateful for the comments we received from anonymous
   referees.
 
-  \bibliographystyle{plain}
-  \bibliography{root}
+  %\bibliographystyle{plain}
+  %\bibliography{root}
 *}