diff -r 83ba2d8c859a -r d37703e0c5c4 PIPBasics.thy --- a/PIPBasics.thy Thu Jan 14 00:55:54 2016 +0800 +++ b/PIPBasics.thy Sat Jan 16 10:59:03 2016 +0800 @@ -3775,4 +3775,6 @@ definition cps:: "state \ (thread \ precedence) set" where "cps s = {(th, cp s th) | th . th \ threads s}" +find_theorems holding wq + end