# HG changeset patch
# User urbanc
# Date 1328577034 0
# Node ID 5920649c5a229b3ba81cae82e96b26613398963d
# Parent  d296cb127fcbaf35897e9e3dcec4aae58e7524ef
more on paper

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}