--- 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 \<Rightarrow> (thread \<times> precedence) set"
 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 
+find_theorems holding wq
+
 end