equal
deleted
inserted
replaced
196 lemma |
196 lemma |
197 cpreced_def2: |
197 cpreced_def2: |
198 "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})" |
198 "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})" |
199 unfolding cpreced_def image_def |
199 unfolding cpreced_def image_def |
200 apply(rule eq_reflection) |
200 apply(rule eq_reflection) |
201 apply(rule arg_cong) |
201 apply(rule_tac f="Max" in arg_cong) |
202 back |
|
203 by (auto) |
202 by (auto) |
204 (*>*) |
203 (*>*) |
205 |
204 |
206 abbreviation |
205 abbreviation |
207 "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
206 "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |