equal
deleted
inserted
replaced
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 |
3778 |
|
3779 find_theorems "waiting" holding |
|
3780 context valid_trace |
|
3781 begin |
|
3782 |
|
3783 find_theorems "waiting" holding |
3779 |
3784 |
3780 end |
3785 end |
|
3786 |
|
3787 end |