| changeset 77 | d37703e0c5c4 |
| parent 69 | 1dc801552dfd |
| child 80 | 17305a85493d |
| 74:83ba2d8c859a | 77:d37703e0c5c4 |
|---|---|
3773 |
3773 |
3774 -- {* A useless definition *} |
3774 -- {* A useless definition *} |
3775 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
3775 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
3776 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
3776 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
3777 |
3777 |
3778 find_theorems holding wq |
|
3779 |
|
3778 end |
3780 end |