--- a/prio/Paper/Paper.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -375,13 +375,6 @@
   programmer has to ensure this.
 
 
-  {\bf ??? define detached}
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{thm detached_def}
-  \end{isabelle}
-  
-
-
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
 
@@ -543,12 +536,22 @@
   running, namely the one whose current precedence is equal to the maximum of all ready 
   threads. We use sets to capture both possibilities.
   We can now also conveniently define the set of resources that are locked by a thread in a
-  given state.
+  given state
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm holdents_def}
   \end{isabelle}
 
+  \noindent
+  and also when a thread is detached
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm detached_def}
+  \end{isabelle}
+
+  \noindent
+  which means that @{text th} neither holds nor waits for a resource in @{text s}.
+  
   Finally we can define what a \emph{valid state} is in our model of PIP. For
   example we cannot expect to be able to exit a thread, if it was not
   created yet. 
@@ -1211,6 +1214,18 @@
   be recalculated for an event. This information is provided by the lemmas we proved.
   We confirmened that our observations translate into practice by implementing
   a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}. 
+  Our events translate in PINTOS to the following function interface:
+
+  \begin{center}
+  \begin{tabular}{|l|l|}
+  \hline
+  {\bf Event} & {\bf PINTOS function} \\
+  \hline
+  @{text Create} & \\
+  @{text Exit}   & \\
+  \end{tabular}
+  \end{center}
+
 *}
 
 section {* Conclusion *}