equal
deleted
inserted
replaced
203 \end{isabelle} |
203 \end{isabelle} |
204 |
204 |
205 \noindent |
205 \noindent |
206 In this definition we set @{text 0} as the default priority for |
206 In this definition we set @{text 0} as the default priority for |
207 threads that have not (yet) been created. The last function we need |
207 threads that have not (yet) been created. The last function we need |
208 calculates the ``time'', or index, at which a process was created. |
208 calculates the ``time'', or index, at which time a process had its |
|
209 priority set. |
209 |
210 |
210 \begin{isabelle}\ \ \ \ \ %%% |
211 \begin{isabelle}\ \ \ \ \ %%% |
211 \mbox{\begin{tabular}{lcl} |
212 \mbox{\begin{tabular}{lcl} |
212 @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & |
213 @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & |
213 @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\ |
214 @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\ |