diff -r 8067efcb43da -r 17305a85493d PIPBasics.thy~ --- a/PIPBasics.thy~ Sun Jan 17 22:18:35 2016 +0800 +++ b/PIPBasics.thy~ Wed Jan 27 19:26:56 2016 +0800 @@ -3775,6 +3775,13 @@ definition cps:: "state \ (thread \ precedence) set" where "cps s = {(th, cp s th) | th . th \ threads s}" -find_theorems readys runing + +find_theorems "waiting" holding +context valid_trace +begin + +find_theorems "waiting" holding end + +end