--- a/prio/Paper/Paper.thy	Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Apr 20 14:15:36 2012 +0000
@@ -38,8 +38,9 @@
   original_priority ("priority") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 
-abbreviation
+(*abbreviation
  "detached s th \<equiv> cntP s th = cntV s th"
+*)
 (*>*)
 
 section {* Introduction *}
@@ -375,6 +376,10 @@
 
 
   {\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