diff -r d296cb127fcb -r 5920649c5a22 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Feb 07 00:50:23 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 07 01:10:34 2012 +0000
@@ -205,7 +205,8 @@
   \noindent
   In this definition we set @{text 0} as the default priority for
   threads that have not (yet) been created. The last function we need 
-  calculates the ``time'', or index, at which a process was created.
+  calculates the ``time'', or index, at which time a process had its 
+  priority set.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}