equal
deleted
inserted
replaced
267 critical resources are free (or unlocked). This status is represented by |
267 critical resources are free (or unlocked). This status is represented by |
268 the abbreviation @{text "all_unlocked"}. |
268 the abbreviation @{text "all_unlocked"}. |
269 *} |
269 *} |
270 |
270 |
271 abbreviation |
271 abbreviation |
272 "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
272 "all_unlocked \<equiv> \<lambda>cs::cs. ([]::thread list)" |
273 |
273 |
274 |
274 |
275 text {* |
275 text {* |
276 |
276 |
277 \noindent The initial current precedence for a thread can be anything, |
277 \noindent The initial current precedence for a thread can be anything, |