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