--- a/prio/Paper/Paper.thy	Mon Apr 16 15:08:24 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Apr 16 15:16:02 2012 +0000
@@ -93,7 +93,7 @@
   implemented. This includes VxWorks (a proprietary real-time OS used
   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
   ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
-  example in libraries for FreeBSD, Solaris and Linux. ({\bf Is this True?})
+  example in libraries for FreeBSD, Solaris and Linux. ({\bf ??? Is this True?})
 
   One advantage of PIP is that increasing the priority of a thread
   can be dynamically calculated by the scheduler. This is in contrast
@@ -375,7 +375,7 @@
   programmer has to ensure this.
 
 
-  {\bf define detached}
+  {\bf ??? define detached}
 
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
@@ -1247,7 +1247,7 @@
   provide this kind of ``deep understanding'' about the principles behind 
   PIP and its correctness.
 
-  {\bf rewrite the following slightly}
+  {\bf ??? rewrite the following slightly}
 
   PIP is a scheduling algorithm for single-processor systems. We are
   now living in a multi-processor world. So the question naturally
@@ -1275,7 +1275,7 @@
   PVS of the Priority Ceiling Protocol done by Dutertre
   \cite{dutertre99b}---another solution to the Priority Inversion
   problem, which however needs static analysis of programs in order to
-  avoid it. {\bf mention model-checking approaches}
+  avoid it. {\bf ??? mention model-checking approaches}
 
   Our formalisation
   consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
@@ -1286,7 +1286,7 @@
   can be downloaded from
   \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
 
-  {\bf say:
+  {\bf ??? say:
   So this paper is a good witness for one
 of the major reasons to be interested in machine checked reasoning:
 gaining deeper understanding of the subject matter.